Swapping Program Variables

Although this is a trivial example, it gives a gentle introduction to the the way in which refinement laws are used. A procedure that swaps the values of two variables is specified as follows:

     PROCEDURE Swap(x,y:T)
       x,y:=x',y' | x'=y /\ y'=x        <--

In order to implement this in a language that doesn't contain simultaneous assignment, we need to introduce a local variable to temporarily hold one of the values. For the moment, we forget about the first line of the above specification and just focus on the line marked with a "<--". Using the Introduce Local Variable Law we can refine this by introducing a local variable t that gets assigned the value of x. The law is as follows:

Introduce Local Variable Law:

     {pre} v:=v' | rel
   [=
      VAR l:T . l:=E;  {pre} v,l:=v',l' | rel 

By matching "t" with "l", "x,y" with "v", "x" with "E", "true" with "pre" and "x'=y /\ y'=x" with "rel", the law tells us that

      x,y:=x',y' | x'=y /\ y'=x
   [=
     VAR t:T .  
     t:=x ;
     x,y,t:=x',y',t' | x'=y /\ y'=x

Thus the body of the swap specification (marked with a "<--" above) may be replaced by the program:

     VAR t:T .  
     t:=x ;                                <--
     x,y,t:=x',y',t' | x'=y /\ y'=x        <--

Again we focus on the marked lines. In order to be able to make use of the fact that t now has the value of x we introduce an assertion after the first assignment:

t:=x ;
{ t=x }
x,y,t:=x',y',t' | x'=y /\ y'= x <--

Notice that the Introduce Assert Law is a conditional law since it is only valid if the condition "E doesn't mention v" holds. In this case, the condition is easily shown to hold (x is a variable which is different to t). Later we shall see laws that have more complicated conditions.

The assert can now be used to rewrite the highlighted variable:

     x,y,t:=x',y',t' | x'=y /\ y'=t        <--

We proceed by making a Leading Assignment to x and introducing an assertion after this assignment:

x:=y ;
{ t=x }
{x=y} x,y,t:=x',y',t' | x'= y /\ y'=t <--

We can rewrite the highlighted variable:

     x,y,t:=x',y',t' | x'=x /\ y'=t

and decide to leave t unchanged, by strengthening the relation:

     x,y,t:=x',y',t' | t'=t /\ x'=x /\ y'=t

This step depends on the condition

     t'=t /\ x'=x /\ y'=t   ==>   x'=x /\ y'=t,

which clearly holds.

The program can then be simplified by contracting the frame:

     y:=y' | y'=t

which is refined to an assignment using the Introduce Assignment Law:

     y:=t

Gathering the refined components together, we get an implementation of the Swap procedure:

     PROCEDURE Swap(x,y:T)
     VAR t:T .
      t:=x ;
      x:=y ;
      y:=t