pi = 3  # sorry --- the checker handles  int  only  )-:
c = 0

def circ(diameter) :
    """{ pre  diameter >= 0  and  pi >= 3
         post  c == pi * diameter  
    }"""
    global c   # this designates that global c will be updated
    c = pi * diameter


"""{ 1.OK pi == 3   premise 
     2.OK pi >= 3   algebra 1
}"""
novar = circ(2)
"""{ 1.OK  c == pi * 2   premise }"""