{ 
m < #t /\
setm
} ;
IF k in
(dom (abs t)) ... FI
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:
{
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:=
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\
We do some rewriting to get:
{ m<#t /\ inv }
m:=m' |
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