def succ(x) : """{ pre True post y > x return y }""" #PREMISES FOR NEXT LINE: # True x = x - 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (x == (x_old - 1)) # True #PREMISES FOR NEXT LINE: y = x + 1 #PREMISES FOR ATTACHED PROOF, IF ANY: # (y == (x + 1)) #PREMISES FOR NEXT LINE: # (y == (x + 1)) return y #PREMISES FOR NEXT LINE: # (y > x) # ERROR: sorry: cannot assign to input parameter x #PREMISES FOR NEXT LINE: a = succ(2) #PREMISES FOR ATTACHED PROOF, IF ANY: # (a > 2) #PREMISES FOR NEXT LINE: # (a > 2)