### MODULE ######################################## pi = 3 # sorry --- the checker handles ints only )-: #PREMISES FOR ATTACHED PROOF, IF ANY: # (pi == 3) #PREMISES FOR NEXT LINE: # (pi == 3) c = 0 #PREMISES FOR ATTACHED PROOF, IF ANY: # (c == 0) # (pi == 3) """{ 1.OK c == 0 premise 2.OK c >= 0 algebra 1 }""" #PREMISES FOR NEXT LINE: # (c >= 0) """{ globalinvOK c >= 0 globalinvOK pi == 3 }""" #PREMISES FOR NEXT LINE: # (pi == 3) def circ(diameter) : """{ pre diameter >= 0 post c == pi * diameter }""" global c #PREMISES FOR NEXT LINE: # (diameter >= 0) # (c >= 0) # as needed, we can introduce the two globalinvs into the proof: c = pi * diameter #PREMISES FOR ATTACHED PROOF, IF ANY: # (c == (pi * diameter)) # (diameter >= 0) # (c_old >= 0) """{ 1.OK c == pi * diameter premise 2.OK diameter >= 0 premise 3.OK pi == 3 globalinv 4.OK c >= 0 algebra 1 2 3 5.OK return 1 4 # returns _two_ premises to show # that post proved and globalinv proved }""" #PREMISES FOR NEXT LINE: # (c == (pi * diameter)) # (c >= 0) #PREMISES FOR NEXT LINE: # (pi == 3) ### END ######################################### # this part would be in another component that imports (uses) the module: """{ 1.OK pi == 3 globalinv 2.OK c >= 0 globalinv }""" #PREMISES FOR NEXT LINE: # (c >= 0) novar = circ(2) #PREMISES FOR ATTACHED PROOF, IF ANY: # (c == (pi * 2)) # (c_old >= 0) """{ 1.OK c == pi * 2 premise 2.OK c >= 0 globalinv }""" #PREMISES FOR NEXT LINE: # (c >= 0)