def absValue(x) : """{ pre x != 0 post ans > 0 return ans }""" if x < 0 : """{ 1.OK x != 0 premise 2.OK x < 0 premise }""" ans = 0 - x """{ 1.OK x < 0 premise 2.OK ans == 0 - x premise 3.OK ans > 0 algebra 1 2 }""" else : """{ 1.OK x != 0 premise 2.OK not(x < 0) premise 3.OK x >= 0 algebra 2 4.OK x > 0 algebra 1 3 }""" ans = x """{ 1.OK ans == x premise 2.OK x > 0 premise 3.OK ans > 0 subst 1 2 }""" """{ 1.OK ans > 0 premise }""" # that is, we proved (ans > 0 or ans > 0), which is ans > 0 return ans # we proved the postcondition m = readInt() assert m <= 0 n = m - 1 """{ 1.OK m <= 0 premise 2.OK n == m - 1 premise 3.OK m <= 0 and n == m - 1 andi 1 2 4.OK n-1 != 0 algebra 1 2 5.OK n-1 != 0 and (m <= 0 and n == m - 1) andi 4 3 }""" m = absValue(n-1) """{ 1.OK m > 0 premise 2.OK n-1 != 0 and (m_old <= 0 and n == m_old - 1) premise 3.OK m_old <= 0 and n == m_old - 1 ande 2 4.OK n - 1 <= 0 algebra 3 5.OK m > 0 and n - 1 <= 0 andi 1 4 }"""