### 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)