def double(a): """returns a list b that holds all of a's values * 2 (see post)""" """{ pre True post forall 0 <= i < len(a), b[i] == a[i] * 2 return b }""" b = [] #PREMISES FOR ATTACHED PROOF, IF ANY: # (b == []) # True #PREMISES FOR NEXT LINE: # (b == []) x = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (x == 0) # (b == []) """{ 1.OK forall 0 <= i < x, b[i] == a[i] * 2 foralli 2.OK x == len(b) algebra }""" #PREMISES FOR NEXT LINE: # (x == len(b)) while x != len(a) : """{ invariant (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b)) modifies x, b }""" #PREMISES FOR LOOP BODY: # (x != len(a)) # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b))) b.append(a[x]*2) #PREMISES FOR ATTACHED PROOF, IF ANY: # (b[(len(b) - 1)] == (a[x] * 2)) # (len(b) == (len(b_old) + 1)) # (x != len(a)) # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b_old))) """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b_old)) premise 2.OK x == len(b_old) ande 1 10.OK forall 0 <= i < x, b[i] == a[i] * 2 ande 1 3.OK len(b) == len(b_old) + 1 premise 4.OK x == len(b)-1 algebra 2 3 5.OK b[len(b)-1] == a[x]*2 premise 6.OK b[x] == a[x]*2 subst 4 5 7.OK forall 0 <= i < x+1, b[i] == a[i] * 2 foralli 10 6 8.OK len(b) == x + 1 algebra 4 9.OK return 7 8 }""" #PREMISES FOR NEXT LINE: # forall(0, (x + 1), lambda i: (b[i] == (a[i] * 2))) # (len(b) == (x + 1)) x = x + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (x == (x_old + 1)) # forall(0, (x_old + 1), lambda i: (b[i] == (a[i] * 2))) # (len(b) == (x_old + 1)) """{ 1.OK forall 0 <= i < x_old +1, b[i] == a[i] * 2 premise 2.OK x == x_old +1 premise 3.OK forall 0 <= i < x, b[i] == a[i] * 2 subst 2 1 4.OK len(b) == x_old + 1 premise 5.OK len(b) == x subst 2 4 6.OK x == len(b) algebra 5 #7.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b)) andi 3 6 8. return 3 6 }""" #PREMISES FOR NEXT LINE: # forall(0, x, lambda i: (b[i] == (a[i] * 2))) # (x == len(b)) #PREMISES FOR NEXT LINE: # (forall(0, x, lambda i: (b[i] == (a[i] * 2))) and (x == len(b))) # not (x != len(a)) """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b)) premise 3.OK not(x != len(a)) premise 4.OK x == len(a) algebra 6.OK forall 0 <= i < x, b[i] == a[i] * 2 ande 1 5.OK forall 0 <= i < len(a), b[i] == a[i] * 2 subst 4 6 }""" #PREMISES FOR NEXT LINE: # forall(0, len(a), lambda i: (b[i] == (a[i] * 2))) return b #PREMISES FOR NEXT LINE: # forall(0, len(a), lambda i: (b[i] == (a[i] * 2))) #PREMISES FOR NEXT LINE: