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 }"""