2.9.4 The Final Second Refinement

\includegraphics[width=7mm]{img/pencil_64.png}

MACHINE

Celebrity_2

REFINES

Celebrity_1

SEES

Celebrity_c0

VARIABLES
$\tt  r $
$\tt  R $
$\tt  b $
INVARIANTS
$\tt  inv1 :$

$\it  R \subseteq P $

$\tt  inv2 :$

$\it  b \in P $

$\tt  inv3 :$

$\it  b \notin R $

$\tt  inv4 :$

$\it  Q = R \mathbin {\mkern 1mu\cup \mkern 1mu}\{  b\}  $

EVENTS
Initialisation
begin
$\tt  act1 :$

$\it  r :\in P $

$\tt  act2 :$

$\it  b, R :| b’ \in P \land R’ = P \setminus \{  b’\}  $

end
Event

celebrity $\mathrel {\widehat=}$

refines

celebrity

when
$\tt  grd1 :$

$\it  R = \emptyset $

with
$\tt  x :$

$\tt  b=x $

then
$\tt  act1 :$

$\it  r := b $

end
Event

remove_1 $\mathrel {\widehat=}$

refines

remove_1

any
$\it  x $
where
$\tt  grd1 :$

$\it  x \in R $

$\tt  grd2 :$

$\it  x \mapsto b \in k $

with
$\tt  y :$

$\tt  b=y $

then
$\tt  act1 :$

$\it  R := R \setminus \{  x\}  $

end
Event

remove_2 $\mathrel {\widehat=}$

refines

remove_2

any
$\it  x $
where
$\tt  grd1 :$

$\it  x \in R $

$\tt  grd2 :$

$\it  x \mapsto b \notin k $

with
$\tt  y :$

$\tt  b=y $

then
$\tt  act2 :$

$\it  b := x $

$\tt  act1 :$

$\it  R := R \setminus \{  x\}  $

end
END