Example: Swapping variables

As a first example we consider two versions of a program exchanging the values of two variables. The first (and standard) solution uses a temporary variable:

        { x = A and y = B}
          temp := x ;
          x := y ;
          y := temp
        { x = B and y = A }

The second version shows that two integer values may be interchanged without an auxiliary variable. Both versions can be entered into NPPV as shown and will be automatically proved correct.

        { x = A and y = B}
          x := x+y ;
          y := x-y ;
          x := x-y
        { x = B and y = A }