Rodin Handbook





 
Previous: The Celebrity Problem Up: Proving Next: The Celebrity algorithm User Manual for Rodin v.2.3

Feedback

2.9.2 The Final Second Refinement

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
Previous: The Celebrity Problem Up: Proving Next: The Celebrity algorithm  
User Manual for Rodin v.2.3 : Tutorial : Proving : The Final Second Refinement