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