## 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
```