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
       temp-mem(insert(F,insert(F,S))) = temp-mem(insert(F,S))     and
       U:User (not-ack(U,insert(F,insert(F,S))) = not-ack(U,insert(F,S))) )
    • Quantifier elimination introduces new constants f :Elt and s :State .
    • Conjunction elimination introduces subgoals as follows:
      1. (database(insert(f,insert(f,s))) = database(insert(f,s))) .
        • Show (database(insert(f,insert(f,s))) = database(insert(f,s))) by reduction.
      2. (temp-mem(insert(f,insert(f,s))) = temp-mem(insert(f,s))) .
        • Show (temp-mem(insert(f,insert(f,s))) = temp-mem(insert(f,s))) by reduction.
      3. forall U:User (not-ack(U,insert(f,insert(f,s))) = not-ack(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
       temp-mem(submit(F,submit(F,S))) = temp-mem(submit(F,S))     and
       U:User (not-ack(U,submit(F,submit(F,S))) = not-ack(U,submit(F,S))) )
    • Quantifier elimination introduces new constants f :Elt and s :State .
    • Conjunction elimination introduces subgoals as follows:
      1. (database(submit(f,submit(f,s))) = database(submit(f,s))) .
        • Show (database(submit(f,submit(f,s))) = database(submit(f,s))) by reduction.
      2. (temp-mem(submit(f,submit(f,s))) = temp-mem(submit(f,s))) .
        • Show (temp-mem(submit(f,submit(f,s))) = temp-mem(submit(f,s))) by reduction.
      3. forall U:User (not-ack(U,submit(f,submit(f,s))) = not-ack(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
       temp-mem(receive(F,receive(F,S))) = temp-mem(receive(F,S))     and
       U:User (not-ack(U,receive(F,receive(F,S))) = not-ack(U,receive(F,S))) )
    • Quantifier elimination introduces new constants f :Elt and s :State .
    • Conjunction elimination introduces subgoals as follows:
      1. (database(receive(f,receive(f,s))) = database(receive(f,s))) .
        • Show (database(receive(f,receive(f,s))) = database(receive(f,s))) by reduction.
      2. (temp-mem(receive(f,receive(f,s))) = temp-mem(receive(f,s))) .
        • Show (temp-mem(receive(f,receive(f,s))) = temp-mem(receive(f,s))) by reduction.
      3. forall U:User (not-ack(U,receive(f,receive(f,s))) = not-ack(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
       temp-mem(ack(U',F,ack(U',F,S))) = temp-mem(ack(U',F,S))     and
       U:User (not-ack(U,ack(U',F,ack(U',F,S))) = not-ack(U,ack(U',F,S))) )
    • Quantifier elimination introduces new constants f :Elt and u' :User and s :State .
    • Conjunction elimination introduces subgoals as follows:
      1.    database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s))     and
           temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s))
        • Conjunction elimination introduces subgoals as follows:
          1. (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.
          2. (temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s)))
            • Show (temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s))) by reduction.
      2. U:User (not-ack(U,ack(u',f,ack(u',f,s))) = not-ack(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
          1. (u1 = u) implies (not-ack(u,ack(u',f,ack(u',f,s))) = not-ack(u,ack(u',f,s)))
          2. (u1 =\= u) implies (not-ack(u,ack(u',f,ack(u',f,s))) = not-ack(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,