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) """{ 1.OK x != 0 premise 2.OK x < 0 premise }""" #PREMISES FOR NEXT LINE: # (x < 0) ans = 0 - x #PREMISES FOR ATTACHED PROOF, IF ANY: # (ans == (0 - x)) # (x < 0) """{ 1.OK x < 0 premise 2.OK ans == 0 - x premise 3.OK ans > 0 algebra 1 2 }""" #PREMISES FOR NEXT LINE: # (ans > 0) else : #PREMISES FOR ELSE-ARM: # not (x < 0) # (x != 0) """{ 1.OK x != 0 premise 2.OK not(x < 0) premise 3.OK x >= 0 algebra 2 4.OK x > 0 algebra 1 3 }""" #PREMISES FOR NEXT LINE: # (x > 0) ans = x #PREMISES FOR ATTACHED PROOF, IF ANY: # (ans == x) # (x > 0) """{ 1.OK ans == x premise 2.OK x > 0 premise 3.OK ans > 0 subst 1 2 }""" #PREMISES FOR NEXT LINE: # (ans > 0) #PREMISES FOR NEXT LINE: # (ans > 0) # (x != 0) """{ 1.OK ans > 0 premise }""" #PREMISES FOR NEXT LINE: # (ans > 0) # that is, we proved (ans > 0 or ans > 0), which is ans > 0 return ans #PREMISES FOR NEXT LINE: # (ans > 0) #PREMISES FOR NEXT LINE: # we proved the postcondition