def absValue(x) : """{ pre x != 0 post ans > 0 return ans }""" #PREMISES FOR NEXT LINE: # (x != 0) if x < 0 : #PREMISES FOR THEN-ARM: # (x < 0) # (x != 0) ans = 0 - x #PREMISES FOR ATTACHED PROOF, IF ANY: # (ans == (0 - x)) # (x < 0) # (x != 0) #PREMISES FOR NEXT LINE: # (ans == (0 - x)) # (x < 0) # (x != 0) else : #PREMISES FOR ELSE-ARM: # not (x < 0) # (x != 0) ans = x #PREMISES FOR ATTACHED PROOF, IF ANY: # (ans == x) # not (x < 0) # (x != 0) #PREMISES FOR NEXT LINE: # (ans == x) # not (x < 0) # (x != 0) #PREMISES FOR NEXT LINE: # (((ans == (0 - x)) and (x < 0)) or ((ans == x) and not (x < 0))) # (x != 0) return ans #PREMISES FOR NEXT LINE: # (((ans == (0 - x)) and (x < 0)) or ((ans == x) and not (x < 0))) # (x != 0) # (ans > 0) #PREMISES FOR NEXT LINE: