theory Bakery_defs
use import int.Int
type t = Idle | Wait | Crit | Crash
function a int : t
function a' int : t
end
theory Bakery_invpreds
use import int.Int
use import Bakery_defs
predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit)
predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = Crit /\
(a' z2) = Crit)
predicate invariant3 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = Crit /\
(a z2) = Wait)
predicate invariant3' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = Crit /\
(a' z2) = Wait)
end
theory Bakery_trdefs
use import int.Int
use import Bakery_defs
predicate transition__tr3 =
(exists z:int.
(
(a z) = Crit) /\
(
(forall j:int.
if j = z then
a' j = Idle
else a' j = (a j))))
predicate transition__tr2 =
(exists z:int.
(
(a z) = Wait) /\
(
(forall j:int.
if j = z then
a' j = Crit
else if z < j then
a' j = (a j)
else if j < z /\
(a j) = Idle then
a' j = Idle
else a' j = Crash)))
predicate transition__tr1 =
(exists z:int.
(
(a z) = Idle) /\
(
(forall j:int.
if j = z then
a' j = Wait
else if j < z then
a' j = (a j)
else if z < j /\
(a j) = Idle then
a' j = (a j)
else a' j = Crash)))
predicate tau =
(transition__tr1 \/ transition__tr2 \/ transition__tr3)
end
theory Bakery_initialisation
use import int.Int
use import Bakery_defs
use import Bakery_invpreds
predicate init =
forall z:int. ((a z) = Idle)
goal initialisation:
init -> (invariant3 /\ invariant1)
end
theory Bakery_property
use import int.Int
use import Bakery_defs
use import Bakery_invpreds
goal property:
(invariant3 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit))
end
theory Bakery_hint_1
use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
lemma hint_1:
(invariant1 /\ invariant3 /\ tau)
-> invariant1'
end
theory Bakery_hint_2
use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
lemma hint_2:
(invariant3 /\ tau)
-> invariant3'
end
theory Bakery_preservation
use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
use import Bakery_hint_2
use import Bakery_hint_1
goal preservation:
(invariant3 /\ invariant1 /\ tau)
->
(invariant3' /\ invariant1')
end