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:
      1. (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.
      2. (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.
      3. 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
          1. 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.
          2. u' =\= u     implies
                not-ack(u,ack(u', f1,submit(f2,s))) = not-ack(u,submit(f2, ack(u',f1,s)))

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