** Next:** Existence of pids
** Up:** Equivalence of the two
** Previous:** Equivalence of the two

##

Equivalence of the two semantics
of the Close-operator

To prove
, for any non-nested Splice program ,
first observe
that it is rather straightforward to prove that if
then
.
The proof proceeds by induction on the structure of ,
which is possible in PVS because we have defined programs as
an abstract data type.
Most cases are trivial, only for the statement one
has to observe that given a strict total order on the events,
this order can be used as the required order on the read events
and also as the local order for each process identity.

The proof that
implies
also proceeds by induction on .
The main issue here is again the proof for the statement;
given a strict total order on all read events () and
for each process identifier a total order on all events (--see the
definition of
),
we have to construct a global strict total order on all events.

To do this, we introduced in PVS an axiom
stating that
there exists some total order
on
the set of all events
.
This order is used to construct a so-called
minimal extension of
the order on the read events:

The idea is that write events are
ordered as early as possible in the sense that any read event that
does not preceed a write event in
is ordered after by .
Hence this minimal extension orders all write events
not later than any of the local orders.
We have proved that this minimal extension satisfies the condition on the
read events in the definition of the global semantics
(which is equal to the one in the definition of
),
because this condition
is invariant under the operation of ordering write events earlier.

** Next:** Existence of pids
** Up:** Equivalence of the two
** Previous:** Equivalence of the two
Roel Bloo
1999-11-26