a = 0
"""{ globalinvOK  a >= 0 }"""

def f(x) :
    """{ pre x > 0
         post ans > 0 
         return ans  }"""
    global a
    ans = (a + x) + 1
    return ans

b = f(1)
print "b =", b