a = 0 """{ globalinvOK a >= 0 }""" def f(x) : """{ pre x > 0 post ans > x and ans > a return ans }""" global a ans = (a + x) + 1 return ans b = 1 c = f(b) """{ 1.OK c > b and c > a premise 3.OK a >= 0 globalinv 4.OK c > 0 algebra 1 3 }"""