Information Technology Reference
In-Depth Information
1:
definition
2:
≡
do {
"set_enum S
←
FOREACHi
3:
(_, m)
4:
(set_enum__foreachi S)
5:
S
(
ʻ
x (k, m). RETURN (Suc k, m(x
ₒ
k)))
6:
7:
(1, empty);
RETURN (
ʻ
x. case m x of None
⃒
0 | Some k
⃒
k) }"
8:
Fig. 4.
Numbering of sets
is the (
i
1)th colouring and is initialised to the function that colours each state
as 1;
C
is the
i
th colouring and is initialised to the function that colours each
accepting state as 1 and all others as 2. We need
C
and
C
in order to determine
whether the current iteration has actually refined the current colouring.
Line 9 performs a kind of nondeterministic assignment: the term following it
is essentially a set of values, and an element of this set is assigned to (
,C
,
)
nondeterministically. The refinement framework allows us to specify algorithms
with such nondeterminism, prove theorems about them, and replace the nonde-
terminism by a deterministic implementation later and independently.
Back to the code: line 10 contains the
while
-construct in this language. Its
first argument (line 11) consists of a loop invariant that must be provided by the
programmer and that is used in correctness proofs. The second argument (line
12) is the loop condition corrected as explained in Sec. 3.1. The third argument
(lines 13 to 21) is the loop body which takes the form of a
ʻ
-term with an
abstraction over (
C,C
,i
), applied to the argument (
C,C
,i
) (line 21) which
corresponds to the initial values explained two paragraphs above.
During each iteration, a new colouring is computed in the form of a function
f
that assigns a certain triple to each state;
R
is then defined as the image of
f
on
Q
, i.e.,
R
is the set of all the colours of the new colouring. In order to convert
those complicated triples into simple numbers, an auxiliary function shown in
Fig. 4 is used;
fi
, obtained by a nondeterministic assignment as in line 9, is then
the numbering of
R
. The new colouring is then the composition of
fi
and
f
.It
assigns a number to each state.
The function
set enum
computes the set of all unique numberings for a set
S
,sothat
set enum S
is the set of bijections between
S
and
−
.The
definition of the function starts with a
foreach
-construct (lines 3-7). In line 3
one possible result of the loop is chosen non-deterministically and is assigned
to (
,m
). In the following line a loop-invariant is provided in order to be able
to prove correctness properties of the definition. The second parameter in line 5
represents the iterated set. For each element of
S
the body of the loop (line 6) is
applied sequentially in an arbitrary order, where
x
is an element of
S
and (
k,m
)
an intermediate result of the loop, that is propagated through the iterations
starting with (1
, empty
). Such results correspond to a pair consisting of the next
number to assign and an already constructed mapping of numbers to elements
{
1
,...,
#
S
}
