Rodin User’s Handbook v.2.8: The Final Second Refinement

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

Rodin Handbook

2.9.4 The Final Second Refinement