Properties of the Tatami Protocol
Idemopotency of insert.
We want to prove
F:Elt (S:State (insert(F,insert(F,S)) = insert(F,S)))
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
 First, we prove the attribute coherence of the input specification.
 Introduce the
lemma
coherence(PROTOCOL)
.
 This goal is true because
coherence(PROTOCOL)
is in the hypothesis.
 Then we prove
F:Elt
S:State
(database(insert(F,insert(F,S))) = database(insert(F,S)) and
tempmem(insert(F,insert(F,S))) = tempmem(insert(F,S)) and
U:User (notack(U,insert(F,insert(F,S))) = notack(U,insert(F,S))) )
 Quantifier elimination introduces new
constants f :Elt and s :State
.
 Conjunction elimination introduces subgoals as follows:

(database(insert(f,insert(f,s))) = database(insert(f,s)))
.
 Show
(database(insert(f,insert(f,s))) = database(insert(f,s)))
by reduction.

(tempmem(insert(f,insert(f,s))) = tempmem(insert(f,s)))
.
 Show
(tempmem(insert(f,insert(f,s))) = tempmem(insert(f,s)))
by reduction.

forall U:User (notack(U,insert(f,insert(f,s))) = notack(U,insert(f,s)))
.
Properties of the Tatami Protocol
Idemopotency of submit.
We want to prove
F:Elt (S:State (submit(F,submit(F,S)) = submit(F,S)))
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
 First, we prove the attribute coherence of the input specification.
 Introduce the
lemma
coherence(PROTOCOL)
.
 This goal is true because
coherence(PROTOCOL)
is in the hypothesis.
 Then we prove
F:Elt
S:State
(database(submit(F,submit(F,S))) = database(submit(F,S)) and
tempmem(submit(F,submit(F,S))) = tempmem(submit(F,S)) and
U:User (notack(U,submit(F,submit(F,S))) = notack(U,submit(F,S))) )
 Quantifier elimination introduces new
constants f :Elt and s :State
.
 Conjunction elimination introduces subgoals as follows:

(database(submit(f,submit(f,s))) = database(submit(f,s)))
.
 Show
(database(submit(f,submit(f,s))) = database(submit(f,s)))
by reduction.

(tempmem(submit(f,submit(f,s))) = tempmem(submit(f,s)))
.
 Show
(tempmem(submit(f,submit(f,s))) = tempmem(submit(f,s)))
by reduction.

forall U:User (notack(U,submit(f,submit(f,s))) = notack(U,submit(f,s)))
.
Properties of the Tatami Protocol
Idemopotency of receive.
We want to prove
F:Elt (S:State (receive(F,receive(F,S)) = receive(F,S)))
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
 First, we prove the attribute coherence of the input specification.
 Introduce the
lemma
coherence(PROTOCOL)
.
 This goal is true because
coherence(PROTOCOL)
is in the hypothesis.
 Then we prove
F:Elt
S:State
(database(receive(F,receive(F,S))) = database(receive(F,S)) and
tempmem(receive(F,receive(F,S))) = tempmem(receive(F,S)) and
U:User (notack(U,receive(F,receive(F,S))) = notack(U,receive(F,S))) )
 Quantifier elimination introduces new
constants f :Elt and s :State
.
 Conjunction elimination introduces subgoals as follows:

(database(receive(f,receive(f,s))) = database(receive(f,s)))
.
 Show
(database(receive(f,receive(f,s))) = database(receive(f,s)))
by reduction.

(tempmem(receive(f,receive(f,s))) = tempmem(receive(f,s)))
.
 Show
(tempmem(receive(f,receive(f,s))) = tempmem(receive(f,s)))
by reduction.

forall U:User (notack(U,receive(f,receive(f,s))) = notack(U,receive(f,s)))
.
Properties of the Tatami Protocol
Idemopotency of ack.
We want to prove
U':User
F:Elt
S:State
ack(U',F,ack(U',F,S)) = ack(U',F,S)
.
We use attribute coinduction to prove this is a behavorial property of the input specification.
 First, we prove the attribute coherence of the input specification.
 Introduce the
lemma
coherence(PROTOCOL)
.
 This goal is true because
coherence(PROTOCOL)
is in the hypothesis.
 Then we prove
U':User
F:Elt
S:State
(database(ack(U',F,ack(U',F,S))) = database(ack(U',F,S)) and
tempmem(ack(U',F,ack(U',F,S))) = tempmem(ack(U',F,S)) and
U:User (notack(U,ack(U',F,ack(U',F,S))) = notack(U,ack(U',F,S))) )
 Quantifier elimination introduces new
constants f :Elt and u' :User and s :State
.
 Conjunction elimination introduces subgoals as follows:

database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s)) and
tempmem(ack(u',f,ack(u',f,s))) = tempmem(ack(u',f,s))
 Conjunction elimination introduces subgoals as follows:

(database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s)))
 Show
(database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s)))
by reduction.

(tempmem(ack(u',f,ack(u',f,s))) = tempmem(ack(u',f,s)))
 Show
(tempmem(ack(u',f,ack(u',f,s))) = tempmem(ack(u',f,s)))
by reduction.

U:User (notack(U,ack(u',f,ack(u',f,s))) = notack(U,ack(u',f,s)))
 Quantifier elimination introduces a new constant
u
of sort
User
.
 Case analysis uses the lemma
U:User ((U = u) or (U =\= u))
on
u1
to get the following subgoals

(u1 = u) implies (notack(u,ack(u',f,ack(u',f,s))) = notack(u,ack(u',f,s)))
 Implication elimination assumes
u1 = u
.
 Change hypothesis
u1 = u
to rewritng rule.
 Show
(notack(u,ack(u',f,ack(u',f,s))) = notack(u,ack(u',f,s)))
by reduction.

(u1 =\= u) implies (notack(u,ack(u',f,ack(u',f,s))) = notack(u,ack(u',f,s)))
This page was generated
by Kumo on
Fri Jun 12 12:33:44 PDT 1998
from code written by Grigore Rosu,