n = 999 #PREMISES FOR ATTACHED PROOF, IF ANY: # (n == 999) #PREMISES FOR NEXT LINE: # (n == 999) x = 999 #PREMISES FOR ATTACHED PROOF, IF ANY: # (x == 999) # (n == 999) #PREMISES FOR NEXT LINE: # (x == 999) # (n == 999) i = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == 0) # (x == 999) # (n == 999) #PREMISES FOR NEXT LINE: # (i == 0) # (x == 999) # (n == 999) # ERROR: line already exists with this number: 4. n == 999 premise sum = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == 0) # (i == 0) # (x == 999) # (n == 999) assert (sum == (x * i)) # UNABLE TO VERIFY """{ 1.OK i == 0 premise 2.OK sum == 0 premise 3.?? sum == x * i algebra 2 1 # ouch! darn * ! try this: 31.OK sum == x * 0 algebra 2 32.OK sum == x * i subst 1 31 4.OK n == 999 premise 5.OK return 32 4 4.OK n == 999 premise 5.OK return 3 4 }""" #PREMISES FOR NEXT LINE: # (sum == (x * i)) # (n == 999) # INVARIANT VERIFIED ON LOOP ENTRY while i != n : """{ invariant sum == x* i modifies i sum }""" #PREMISES FOR LOOP BODY: # (i != n) # (sum == (x * i)) # (n == 999) sum = sum + x #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == (sum_old + x)) # (i != n) # (sum_old == (x * i)) # (n == 999) """{ 1.OK sum == sum_old + x premise 2.OK sum_old == x * i premise 3.OK sum == (x*i) + x algebra 2 1 }""" #PREMISES FOR NEXT LINE: # (sum == ((x * i) + x)) i = i + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == (i_old + 1)) # (sum == ((x * i_old) + x)) """{ 1.OK i == i_old + 1 premise 2.OK sum == (x * i_old) + x premise 3.OK sum == x * (i_old + 1) algebra 2 4.OK sum == x * i subst 1 3 5.OK sum == x * i subst 1 3 }""" #PREMISES FOR NEXT LINE: # (sum == (x * i)) # INVARIANT VERIFIED AT END OF LOOP BODY #PREMISES FOR NEXT LINE: # (sum == (x * i)) # not (i != n) # (n == 999) """{ 1.OK sum == x* i premise 2.OK not ( i != n) premise 3.OK i == n algebra 2 4.OK sum == x * n subst 3 1 }""" #PREMISES FOR NEXT LINE: # (sum == (x * n))