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) #PREMISES FOR NEXT LINE: # (c == 0) # (pi == 3) def circ(diameter) : """{ pre diameter >= 0 and pi >= 3 post c == pi * diameter }""" global c # this designates that global c will be updated #PREMISES FOR NEXT LINE: # ((diameter >= 0) and (pi >= 3)) c = pi * diameter #PREMISES FOR ATTACHED PROOF, IF ANY: # (c == (pi * diameter)) # ((diameter >= 0) and (pi >= 3)) #PREMISES FOR NEXT LINE: # (c == (pi * diameter)) # ((diameter >= 0) and (pi >= 3)) #PREMISES FOR NEXT LINE: # (c == 0) # (pi == 3) """{ 1.OK pi == 3 premise 2.OK c == 0 premise 3.OK pi > c algebra 1 2 }""" #PREMISES FOR NEXT LINE: # (pi > c) novar = circ(2) # this is a function call that returns no answer #PREMISES FOR ATTACHED PROOF, IF ANY: # (c == (pi * 2)) # (pi > c_old) """{ 1.OK c == pi * 2 premise 2.OK pi > c_old premise # c's value was changed by circ; # this is called a _side effect_ # ... we can do more deductions here ... }""" #PREMISES FOR NEXT LINE: