x = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: n = readInt() #PREMISES FOR ATTACHED PROOF, IF ANY: # True #PREMISES FOR NEXT LINE: i = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == 0) #PREMISES FOR NEXT LINE: # (i == 0) sum = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == 0) # (i == 0) """{ 1.OK sum == 0 premise 2.OK i == 0 premise 3.OK sum == x * 0 algebra 1 4.OK sum == x * i subst 2 3 }""" #PREMISES FOR NEXT LINE: # (sum == (x * i)) # INVARIANT VERIFIED ON LOOP ENTRY while i != n : """{ invariant sum == x* i modifies i, sum }""" #PREMISES FOR LOOP BODY: # (i != n) # (sum == (x * i)) sum = sum + x #PREMISES FOR ATTACHED PROOF, IF ANY: # (sum == (sum_old + x)) # (i != n) # (sum_old == (x * i)) """{ 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 }""" #PREMISES FOR NEXT LINE: # (sum == (x * i)) # INVARIANT VERIFIED AT END OF LOOP BODY #PREMISES FOR NEXT LINE: # (sum == (x * i)) # not (i != n) """{ 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))