Properties of the Tatami Protocol
Commutativity of insert.

We want to prove

F1,F2:Elt S:State insert(F1,insert(F2,S)) = insert(F2, insert(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    (database(insert(F1,insert(F2,S))) = database(insert(F2, insert(F1,S)))     and
       temp-mem(insert(F1,insert(F2,S))) = temp-mem(insert(F2, insert(F1,S)))     and
       U:User (not-ack(U,insert(F1,insert(F2,S))) = not-ack(U,insert(F2, insert(F1,S)))) )
    • Quantifier elimination introduces new constants f1 f2 :Elt and s :State .
    • Introduce the lemma L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) .
    • Change hypothesis L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. (database(insert(f1,insert(f2,s))) = database(insert(f2, insert(f1,s)))) .
        • Show (database(insert(f1,insert(f2,s))) = database(insert(f2, insert(f1,s)))) by reduction.
      2. (temp-mem(insert(f1,insert(f2,s))) = temp-mem(insert(f2, insert(f1,s)))) .
        • Show (temp-mem(insert(f1,insert(f2,s))) = temp-mem(insert(f2, insert(f1,s)))) by reduction.
      3. forall U:User (not-ack(U,insert(f1,insert(f2,s))) = not-ack(U,insert(f2, insert(f1,s)))) .
Properties of the Tatami Protocol

Commutativity of submit.

We want to prove

F1,F2:Elt S:State submit(F1,submit(F2,S)) = submit(F2, submit(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    (database(submit(F1,submit(F2,S))) = database(submit(F2, submit(F1,S)))     and
       temp-mem(submit(F1,submit(F2,S))) = temp-mem(submit(F2, submit(F1,S)))     and
       U:User (not-ack(U,submit(F1,submit(F2,S))) = not-ack(U,submit(F2, submit(F1,S)))) )
    • Quantifier elimination introduces new constants f1 f2 :Elt and s :State .
    • Introduce the lemma L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) .
    • Change hypothesis L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. (database(submit(f1,submit(f2,s))) = database(submit(f2, submit(f1,s)))) .
        • Show (database(submit(f1,submit(f2,s))) = database(submit(f2, submit(f1,s)))) by reduction.
      2. (temp-mem(submit(f1,submit(f2,s))) = temp-mem(submit(f2, submit(f1,s)))) .
        • Show (temp-mem(submit(f1,submit(f2,s))) = temp-mem(submit(f2, submit(f1,s)))) by reduction.
      3. forall U:User (not-ack(U,submit(f1,submit(f2,s))) = not-ack(U,submit(f2, submit(f1,s)))) .
Properties of the Tatami Protocol

Commutativity of receive.

We want to prove

F1,F2:Elt S:State receive(F1,receive(F2,S)) = receive(F2, receive(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    (database(receive(F1,receive(F2,S))) = database(receive(F2, receive(F1,S)))     and
       temp-mem(receive(F1,receive(F2,S))) = temp-mem(receive(F2, receive(F1,S)))     and
       U:User (not-ack(U,receive(F1,receive(F2,S))) = not-ack(U,receive(F2, receive(F1,S)))) )
    • Quantifier elimination introduces new constants f1 f2 :Elt and s :State .
    • Introduce the lemma L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) .
    • Change hypothesis L:Set (add(f1,add(f2,L)) = add(f2,add(f1,L))) to rewritng rule.
    • Conjunction elimination introduces subgoals as follows:
      1. (database(receive(f1,receive(f2,s))) = database(receive(f2, receive(f1,s)))) .
        • Show (database(receive(f1,receive(f2,s))) = database(receive(f2, receive(f1,s)))) by reduction.
      2. (temp-mem(receive(f1,receive(f2,s))) = temp-mem(receive(f2, receive(f1,s)))) .
        • Show (temp-mem(receive(f1,receive(f2,s))) = temp-mem(receive(f2, receive(f1,s)))) by reduction.
      3. forall U:User (not-ack(U,receive(f1,receive(f2,s))) = not-ack(U,receive(f2, receive(f1,s)))) .
Properties of the Tatami Protocol

Commutativity of ack.

We want to prove

F1,F2:Elt U1,U2:User S:State ack(U1,F1,ack(U2,F2,S)) = ack(U2,F2,ack(U1,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 U1,U2:User S:State    (database(ack(U1,F1,ack(U2,F2,S))) = database(ack(U2,F2,ack(U1,F1,S)))     and
       temp-mem(ack(U1,F1,ack(U2,F2,S))) = temp-mem(ack(U2,F2,ack(U1,F1,S)))     and
       U:User (not-ack(U,ack(U1,F1,ack(U2,F2,S))) = not-ack(U,ack(U2,F2,ack(U1,F1,S)))) )
    • Quantifier elimination introduces new constants f1 f2 :Elt and u1 u2 :User and s :State .
    • Introduce the lemma L:Set (del(f1,del(f2,L)) = del(f2,del(f1,L))) .
    • Change hypothesis L:Set (del(f1,del(f2,L)) = del(f2,del(f1,L))) to rewritng rule.
    • Case analysis uses the lemma U:User ((((((U =\= u1) and (U =\= u2)) and (u1 =\= u2)) or ((U =\= u1) and (u1 = u2))) or ((U = u1) and (U =\= u2))) or ((U = u2) and (U =\= u1))) or ((U = u1) and (u2 = u1)) on u to get the following subgoals
      1. ((u =\= u1) and (u =\= u2)) and (u1 =\= u2)     implies
               (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
               U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
        • Implication elimination assumes ((u =\= u1) and (u =\= u2)) and (u1 =\= u2) .
        • Conjunction elimination introduces subgoals as follows:
          1.    database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))
            • Conjunction elimination introduces subgoals as follows:
              1. (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s))))
                • Show (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) by reduction.
              2. (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s))))
                • Show (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) by reduction.
          2. U:User not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))
      2. (u =\= u1) and (u1 = u2)     implies
               (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
               U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
      3. (u = u1) and (u =\= u2)     implies
               (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
               U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
      4. (u = u2) and (u =\= u1)     implies
               (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
               U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
      5. (u = u1) and (u2 = u1)     implies
               (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
               temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
               U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
        • Implication elimination assumes (u = u1) and (u2 = u1) .
        • Change hypothesis (u = u1) and (u2 = u1) to rewritng rule.
        • Conjunction elimination introduces subgoals as follows:
          1. (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) .
            • Show (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) by reduction.
          2. (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) .
            • Show (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) by reduction.
          3. forall U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) .


This page was generated
by Kumo on Fri Jun 12 12:35:10 PDT 1998 from code written by Grigore Rosu,