This example involves the development of a procedure that searches for an entry in a lookup table. The table is implemented as an array of records:

TYPE Table = ARRAY OF RECORD key:Key; item:Item END;

We are not interested in the type of keys and items, so we don't specify it
here. Given a key, the search procedure will try to find an item corresponding
to that key. We assume that each key has at most one entry in the table; this
property is satisfied by a table `t` for which ` uniqueness t`
holds:

uniqueness t == (! m,n < #t. t[m].key = t[n].key ==> m = n)

We can abstract away from the ordering of the records, and just think of a
table as a mapping from keys to items using the `abs` function:

abs t = { (k,i) | ?m<#t. t[m].key = k /\ t[m].item = i }

That is, `k` is mapped to `i` in table `t`, if
there exists an entry whose key is `k` and whose item is `i`.
The uniqueness property ensures that `abs t` is a partial function
rather than a relation. A key `k` has an entry in table `t` if
`k in (dom (abs t))` holds and we can specify the item associated with
key `k` simply as
`(abs t)(k)`.

The search precedure, with full error reporting, is specified as follows:

PROCEDURE Search( t:Table; k:Key; i:Item; r:String ) IF k in (dom (abs t)) THEN i:= (abs t)(k) ; r:= "Found" ELSE r:= "Not Found" FI

We will implement this by simply traversing the table from the start until we either find the key or reach the end of the table. We refine the IF-statement by preceeding it with a statement that sets an index m to the appropriate position in the table (using Introduce Local Variable):

VAR m:Nat . m:=m' | (m' < #t /\ t[m'].key = k) \/ (m' = #t /\ ~(k in (dom (abs t))) ) ; IF k in (dom (abs t)) ... FI

The postcondition for the assignment to `m` says that either `m`
should be given a value less than
`#t`, in which case `m` should index the table entry for `k`,
or `m` should index beyond the end of the table, in which case `k`
has no entry.

Before refining the assignment to `m` further, we
introduce an assertion between it and the
IF-statement. This will be important for refining the IF-statement:

m:=m' | setm' ; <--1 { setm } ; <--2 IF k in (dom (abs t)) ... FI <--2 where setm == (m < #t /\ t[m].key = k) \/ (m = #t /\ ~(k in (dom (abs t))) ) setm' == setm[m\m']

We need to refine both statements 1 and 2, but we can now do this in either
order. Let us proceed with the second statement. Because of the assertion, we
know that the key will have been found if `m<#t` so we
introduce an IF-statement with this condition as
its guard:

IF m < #t THEN { m < #t /\ setm } ; <-- IF k in (dom (abs t)) ... FI <-- ELSE { m = #t /\ setm } ; IF k in (dom (abs t)) ... FI FI

We continue with the first branch:

{ m < #t /\ setm } ;IF k in (dom (abs t)) ... FI

Since

m < #t /\ setm ==> (abs t)(k) = t[m].item

and

(abs t)(k) = t[m].item ==> k in (dom (abs t))

the assertion can be weakened to:

{ k in (dom (abs t)) /\ t(k) = t[m].item } ; IF k in (dom (abs t)) ... FI

or in expanded form:

{ k in (dom (abs t)) /\ t(k) = t[m].item } ; IF k in (dom (abs t)) THEN i:= t(k) ; r:= "Found" ELSE r:= "Not Found" FI

Using the Remove IF-statement Law, this can be refined to

{ t(k) = t[m].item } ;i:= t(k) ;

r:= "Found"

and the assignment to `i` can be
rewritten:

i:= t[m].item ; r:= "Found"

In a similar fashion, the second branch of the IF-statement that we introduced can be refined to:

r:= "Not Found"

So statement 2 is refined by:

IF m < #t THEN i:= t[m].item ; r:= "Found" ELSE r:= "Not Found" FI

We now refine
statement 1. We want to start searching for the key from
the first position of the table, so we
introduce a leading assignment to initialise `m`
to `0`:

m:=0; {m=0} m:=m' | setm' ; <--

We will implement this with a loop that iterates until the key is found, or the end of the table is reached, so we choose the following guard:

G == m<#t /\ ~(t[m].key = k)

We choose an invariant which says that
`m` is within its legal range, and that the key is not in any of the
entries that have already been checked:

inv == 0 <= m <= #t /\ (!n<m . ~(t[n].key = k) )

As a variant, we use the difference between
`m` and the size of `t`:

V = (#t - m)

In order to apply the loop introduction law, we need to show that the following conditions hold:

m=0 ==> inv inv /\ ~G ==> setm

The refined statement is then

DO m<#t /\ ~(t[m].key = k) -> { m<#t /\ ~(t[m].key = k) /\ inv } <-- m:=m' | inv[m\m'] /\ 0 <= #t-m' < #t-m <-- OD

We focus on the loop body, and
strengthen it so that
`m` is incremented by 1:

{ m<#t /\ ~(t[m].key = k) /\ inv }m:=m' | inv[m\m'] /\ 0 <= #t-m' < #t-m /\ m'=m+1

We do some rewriting to get:

{ m<#t /\ inv }m:=m' | inv[m\m+1] /\ 0 <= #t-(m+1) < #t-m /\ m'=m+1

Now we can show that

m<#t /\ ~(t[m].key = k) /\ inv ==> inv[m\m+1] m<#t ==> 0 <= #t-(m+1) < #t-m

so we remove conjuncts to get:

m:=m' | m'=m+1

This is of course implemented by:

m:=m+1

Gathering all the refined components together, we get:

PROCEDURE Search( t:Table; k:Key; i:Item; r:String ) VAR m:Nat . m:=0; DO m<#t /\ ~(t[m].key = k) -> m:=m+1 OD ; IF m < #t THEN i:= t[m].item ; r:= "Found" ELSE r:= "Not Found" FI