Duck Source Code:
Properties of the Tatami Protocol


title:> Properties of the Tatami Protocol
spec:> /net/beowulf/grad/klin/tmp/protocol.obj
dir:> /net/cs/htdocs/groups/tatami/demos/protocol
homepage:> /cse/grad/grosu/tatami/protocol/protocol.hp
specexp:> /cse/grad/grosu/tatami/protocol/spec.ex
author:> Grigore Rosu
<>
**************************************************************************
goal:> coherence(PROTOCOL)
**************************************************************************
:> exp /cse/grad/grosu/tatami/protocol/coherence.ex
:> Coherence 
:> Simplify
:> Simplify
:> Simplify
:> Quantifier-Eli-All
:> Implication-Eli >> [P1:*] 
:> Rewriting-Rule(P1)
:> Conjunction-Eli
:> Conjunction-Eli
:> Simplify
:> Simplify
:> Quantifier-Eli
:> Case-Analyse /net/beowulf/grad/klin/jpq/userlemma u'
:> Simplify
:> Implication-Eli
:> Reduction
<>
****************************************************************************
goal:> forall F:Elt forall S:State insert(F,insert(F,S)) = insert(F,S)
****************************************************************************
:> exp /cse/grad/grosu/tatami/protocol/idempot.ex
:> subtitle:  <b>Idemopotency of insert.</b><hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Simplify
****************************************************************************
goal:> forall F:Elt forall S:State submit(F,submit(F,S)) = submit(F,S)
****************************************************************************
:> subtitle:  <hr><b>Idemopotency of submit</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Simplify
****************************************************************************
goal:> forall F:Elt forall S:State receive(F,receive(F,S)) = receive(F,S)
****************************************************************************
:> subtitle:  <hr><b>Idemopotency of receive</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Simplify
****************************************************************************
goal:> forall U':User forall F:Elt forall S:State ack(U',F,ack(U',F,S)) = ack(U',F,S)
****************************************************************************
:> subtitle:  <hr><b>Idemopotency of ack</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Conjunction-Eli
:> Conjunction-Eli
:> Simplify
:> Simplify
:> Quantifier-Eli
:> Case-Analyse /net/beowulf/grad/klin/jpq/userlemma u1
:> Simplify
:> Implication-Eli
:> Reduction
<>
******************************************************************************
goal:> forall F1:Elt forall F2:Elt forall S:State insert(F1,insert(F2,S)) = insert(F2, insert(F1,S))
******************************************************************************
:> exp /cse/grad/grosu/tatami/protocol/comm.ex
:> subtitle: <b>Commutativity of insert</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Lemma-Introduction     http://www.cs.ucsd.edu/users/klin/tmp/protocol/addass
:> Rewriting-Rule
:> Simplify
******************************************************************************
goal:> forall F1:Elt forall F2:Elt forall S:State submit(F1,submit(F2,S)) = submit(F2, submit(F1,S))
******************************************************************************
:> subtitle: <hr><b>Commutativity of submit</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Lemma-Introduction     http://www.cs.ucsd.edu/users/klin/tmp/protocol/addass
:> Rewriting-Rule
:> Simplify
******************************************************************************
goal:> forall F1:Elt forall F2:Elt forall S:State receive(F1,receive(F2,S)) = receive(F2, receive(F1,S))
******************************************************************************
:> subtitle: <hr><b>Commutativity of  receive</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Lemma-Introduction     http://www.cs.ucsd.edu/users/klin/tmp/protocol/addass
:> Rewriting-Rule
:> Simplify 
**************************************************************************
goal:> forall F1:Elt forall F2:Elt forall U1:User forall U2:User forall S:State ack(U1,F1,ack(U2,F2,S)) = ack(U2,F2,ack(U1,F1,S))
******************************************************************************
:> subtitle: <hr><b>Commutativity of ack</b>.<hr>
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Lemma-Introduction     http://www.cs.ucsd.edu/users/klin/tmp/protocol/delass
:> Rewriting-Rule
:> Case-Analyse /net/beowulf/grad/klin/jpq/userlemma2 u
*** case1
:> Implication-Eli
:> Conjunction-Eli
:> Conjunction-Eli
:> Reduction
:> Reduction
:> Simplify
*** case2
:> Implication-Eli >> [P1:*]
:> Hypo-Conjunction-Eli(P1) >> [P2,P3:*]
:> Rewriting-Rule(P3)
:> Simplify
*** case3
:> Implication-Eli >> [P4:*]
:> Hypo-Conjunction-Eli(P4) >> [P5,P6:*]
:> Rewriting-Rule(P5)
:> Simplify
*** case4
:> Implication-Eli >> [P7:*]
:> Hypo-Conjunction-Eli(P7) >> [P8,P9:*]
:> Rewriting-Rule(P8)
:> Simplify
*** case5
:> Simplify
<>
******************************************************************************
goal:> forall F1:Elt forall F2:Elt forall S:State forall U':User ack(U', F1,submit(F2,S)) = submit(F2, ack(U',F1,S))
******************************************************************************
:> exp /cse/grad/grosu/tatami/protocol/comm.ex
:> A-Coinduction(PROTOCOL)
:> Lemma-Introduction     http://www.cs.ucsd.edu/groups/tatami/demos/protocol/g0 
:> Direct-Check
:> Quantifier-Eli-All
:> Conjunction-Eli-All
:> Simplify
:> Simplify
:> Quantifier-Eli
:> Case-Analyse /net/beowulf/grad/klin/jpq/userlemma u'
:> Simplify
:> Implication-Eli
:> Reduction
<>
*********************************************************************************
goal:> ok?(database(init)) = true
*********************************************************************************
:> exp /cse/grad/grosu/tatami/protocol/correct.ex
:> Simplify
********************************************************************************
goal:> forall S:State  forall F:Elt ( ( ok?(database(S)) = true  and  ok?(parents(F),database(S)) = true) implies  (ok?(database(insert(F,S))) = true and ok?(database(submit(F,S))) = true ))
********************************************************************************
:> Simplify
********************************************************************************
goal:> forall S:State  ( (ok?(database(S)) = true) implies ( ( forall F:Elt ok?(database(receive(F,S))) = true ) and  ( forall F:Elt  forall U:User (ok?(database(ack(U,F,S))) = true)   )))
********************************************************************************
:> Simplify
<>


[Back]
Fri Jun 12 12:32:41 PDT 1998