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: