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:

{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