"""{ defOK mult(0) == 1 defOK mult(n) == mult(n-1) * n }""" #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) fac = 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (fac == 1) # (i == 0) """{ 1.OK mult(0) == 1 def 2.OK fac == 1 premise 3.OK fac == mult(0) algebra 1 2 }""" #PREMISES FOR NEXT LINE: # (fac == mult(0)) # INVARIANT VERIFIED ON LOOP ENTRY while i != n : """{ invariant fac == mult(i) modifies i, fac }""" #PREMISES FOR LOOP BODY: # (i != n) # (fac == mult(i)) """{ 1.OK fac == mult(i) premise }""" #PREMISES FOR NEXT LINE: # (fac == mult(i)) i = i + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (i == (i_old + 1)) # (fac == mult(i_old)) """{ 1.OK i == i_old + 1 premise 2.OK fac == mult(i_old) premise # from the invariant 4.OK fac == mult(i-1) algebra 1 2 }""" #PREMISES FOR NEXT LINE: # (fac == mult((i - 1))) fac = fac * i #PREMISES FOR ATTACHED PROOF, IF ANY: # (fac == (fac_old * i)) # (fac_old == mult((i - 1))) """{ 1.OK fac == fac_old * i premise 2.OK fac_old == mult(i-1) premise 3.OK fac == mult(i-1) * i subst 2 1 4.OK mult(i) == mult(i-1) * i def 5.OK fac == mult(i) subst 4 3 }""" #PREMISES FOR NEXT LINE: # (fac == mult(i)) # INVARIANT VERIFIED AT END OF LOOP BODY #PREMISES FOR NEXT LINE: # (fac == mult(i)) # not (i != n) """{ 1.OK not(i != n) premise 2.OK i == n algebra 1 3.OK fac == mult(i) premise 4.OK fac == mult(n) subst 2 3 }""" #PREMISES FOR NEXT LINE: # (fac == mult(n))