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

def circ(diameter) :
    """{ pre  diameter >= 0  and  pi >= 3
         post  answer == pi * diameter  
         return answer
    }"""
    answer = pi * diameter
    return answer


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