Properties of the Tatami Protocol
We want to prove
F1,F2:Elt
S:State
U':User
ack(U', F1,submit(F2,S)) = submit(F2, ack(U',F1,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
F1,F2:Elt
S:State
U':User
(database(ack(U', F1,submit(F2,S))) = database(submit(F2, ack(U',F1,S))) and
temp-mem(ack(U', F1,submit(F2,S))) = temp-mem(submit(F2, ack(U',F1,S))) and
U:User (not-ack(U,ack(U', F1,submit(F2,S))) = not-ack(U,submit(F2, ack(U',F1,S)))) )
Quantifier elimination introduces new
constants f1 f2 :Elt and u' :User and s :State
.
Conjunction elimination introduces subgoals as follows:
(database(ack(u', f1,submit(f2,s))) = database(submit(f2, ack(u',f1,s))))
.
Show
(database(ack(u', f1,submit(f2,s))) = database(submit(f2, ack(u',f1,s))))
by reduction.
(temp-mem(ack(u', f1,submit(f2,s))) = temp-mem(submit(f2, ack(u',f1,s))))
.
Show
(temp-mem(ack(u', f1,submit(f2,s))) = temp-mem(submit(f2, ack(u',f1,s))))
by reduction.
forall U:User (not-ack(U,ack(u', f1,submit(f2,s))) = not-ack(U,submit(f2, ack(u',f1,s))))
.
Quantifier elimination introduces a new constant
u
of sort
User
.
Case analysis uses the lemma
U:User ((U = u) or (U =\= u))
on
u'
to get the following subgoals
u' = u implies
not-ack(u,ack(u', f1,submit(f2,s))) = not-ack(u,submit(f2, ack(u',f1,s)))
Implication elimination assumes
u' = u
.
Change hypothesis
u' = u
to rewritng rule.
Show
(not-ack(u,ack(u', f1,submit(f2,s))) = not-ack(u,submit(f2, ack(u',f1,s))))
by reduction.
u' =\= u implies
not-ack(u,ack(u', f1,submit(f2,s))) = not-ack(u,submit(f2, ack(u',f1,s)))
Implication elimination assumes
u' =\= u
.
Show
(not-ack(u,ack(u', f1,submit(f2,s))) = not-ack(u,submit(f2, ack(u',f1,s))))
by reduction.
This page was generated
by Kumo on
Fri Jun 12 12:38:16 PDT 1998
from code written by Grigore Rosu,