none
How to prove addition

    Question

  • I want to develop code contracts to prove that a simple function int Add(int a, int b) will return the sum of the two arguments passed to it.

    In digging around I found a proof that uses Peano Postulates:

    The proof starts from the Peano Postulates, which define the natural 
    numbers N. N is the smallest set satisfying these postulates:

      P1.  1 is in N.
      P2.  If x is in N, then its "successor" x' is in N.
      P3.  There is no x such that x' = 1.
      P4.  If x isn't 1, then there is a y in N such that y' = x.
      P5.  If S is a subset of N, 1 is in S, and the implication
           (x in S => x' in S) holds, then S = N.

    Then you have to define addition recursively:
      Def: Let a and b be in N. If b = 1, then define a + b = a'
           (using P1 and P2). If b isn't 1, then let c' = b, with c in N
           (using P4), and define a + b = (a + c)'.

    Then you have to define 2:
      Def:  2 = 1'

    2 is in N by P1, P2, and the definition of 2.

    Theorem:  1 + 1 = 2

    Proof: Use the first part of the definition of + with a = b = 1.
           Then 1 + 1 = 1' = 2  Q.E.D.

    Note: There is an alternate formulation of the Peano Postulates which 
    replaces 1 with 0 in P1, P3, P4, and P5. Then you have to change the 
    definition of addition to this:
      Def: Let a and b be in N. If b = 0, then define a + b = a.
           If b isn't 0, then let c' = b, with c in N, and define
           a + b = (a + c)'.

    You also have to define 1 = 0', and 2 = 1'. Then the proof of the 
    Theorem above is a little different:

    Proof: Use the second part of the definition of + first:
           1 + 1 = (1 + 0)'
           Now use the first part of the definition of + on the sum in
           parentheses:  1 + 1 = (1)' = 1' = 2  Q.E.D.

    - Doctor Rob, The Math Forum
      http://mathforum.org/dr.math/   

    I'd like to know how I can use this to define the contract for my Add function or an alternative.

    Thanks

    Wednesday, May 10, 2017 1:53 PM