Some standard daemons are responsible for the low level communication providing the background mechanism on which the Tatami Protocol is based. However, the Tatami Protocol should be viewed as a collection of strategies saying what to do when certain events are encountered, including the following:

• insert an element in the database, where an element can be a specification, a proof task, an inference rule, a part of a proof, etc.,
• submit an element to all members of the project,
• receive an element from another member of the project; it is left to the daemons to send acknowledgements for the received elements, and
• acknowledge an element received from another user.

• database gives the elements which put together give a consistent proof. Notice that because of the unpredictable way in which messages are carried over the internet, it could be the case that some already received elements depend on other elements which have not yet been received; such elements are not provided by the database attribute.
• temp-mem gives all those elements which cannot be provided by the database attribute. There is no good reason to prevent applications from accessing these elements, but if they do so then, of course, consistency is not guaranteed.
• not-ack gives the communication status of every user, i.e., for each user U , the already submitted messages which have not been acknowledged by U .

It is usually convenient to specify data by initial algebras, but in this example, the algebra of data is specified loosely as a theory of dependency sets, DEP-SET. This means that DEP-SET contains properties that must be respected by any concrete algebra we might chose for data. An interesting and immediate consequence of this approacg is that, depending on what algebra is chosen for data, different classes of systems can be obtained.

We first disscuss dependency sets, that is, sets in which elements may depend on each other. The interesting operations on such sets are as follows:

• parents which gives the set of all parents of an element.
• ok? which takes a set to a boolean value, saying if that set is consistent regarding the dependencies between its elements. We are flexible in defining this concept because it can mean everything in practical situations. One resonable way to define it, which was the first one we considered for the Tatami Protocol, is to say that a set is consistent iff all parents of each element in the set are in the set, too. Another way, which was the second one we considered for the Tatami Protocol, is to ask every element have at least one parent in the set. However, the actual implementation is somewere between, in the sense that some elements are required to have one parent in the set and other operations are required to have more parents in the set. All these made us not define the ok? operation, but only ask some properties it must resprect. In order to do this, we introduced a binary ok? which gives a relation between the parents of an element and the rest of elements. It might be the inclusion of sets (the first approach), the non-empty intersection (the second approach) or everything else.
• l<_,_> and r<_,_> are the main operations in DEP-SET. Informally, l< L , R > gives the largest subset Q of L U R which includes L , such that ok?(Q) is true, and r< L , R > gives the elements in L U R which are not in l< L , R > . We call l<_,_> the left closure and r<_,_> the right closure. These closures are constrained to respect two properties. The firts one (which is given by a pair of equations) regards the idempotency of closures, i.e., taking a closure then adding an element to the right and taking the closure again is the same thing as if the first closure is ignored. The second property is very natural and it says that ok?(l< L , R >) is true whenever ok?(L) is true.

We formally specify the Tatami Protocol as a behavioral specification in which insert, submit, receive and ack are methodes, and database, temp-mem, and not-ack are attributes on a hidden State.

• insert : Elt State -> State takes a state and an element and inserts that element in the database associated with the state, letting everything else unchanged. This is a local operation which allows the user to add new things in his(her) local database. It is assumed that the new inserted element is consistent with the database.
• submit : Elt State -> State is similar to insert in what regards the database and the temp-mem, but it adds the element in the list of not-acknowledged messages of every user in the project. It is daemons' job to phisically send the not acknowledged elements over the internet.
• receive : Elt State -> State is a method which is activated by a receiver daemon each time a new element is received. First, it adds that element to the temporal memory and then it takes the left closure of the actual database and the temporal memory. This is because either the received element might not be delivered to the database yet because of the dependencies, or it can be delivered but, together with it, other elements from the temporal memory should be delivered.
• ack : User Elt State -> State is also going to be activated by a daemon when it receives an acknowledgement from another user of an already submitted message. All it does is delete that acknowledged element from that user's not-acknowledged elements.

In order too prove behavioral properties using attribute coinduction, the attribute coherence of the specification must be checked. In other words, we have to show that a state is fully characterized by observations using only attributes. To do this, we have to prove that S1 =A= S2 implies

1. insert(E, S1) =A= insert(E, S2),
2. submit(E, S1) =A= submit(E, S2),
3. receive(E, S1) =A= receive(E, S2),
4. ack(U, E, S1) =A= ack(U, E, S2),

In the case of ack, this is done by proving the first order formula:

S1,S2:State U':User E:Elt (
       (database(S1) = database(S2) and
        temp-mem(S1) = temp-mem(S2) and
       U:User (not-ack(U,S1) = not-ack(U,S2))

    implies

       (database(ack(U',E,S1)) = database(ack(U',E,S2))     and
        temp-mem(ack(U',E,S1)) = temp-mem(ack(U',E,S2))     and
       U:User (not-ack(U,ack(U',E,S1)) = not-ack(U,ack(U',E,S2))) )

By quatifier elimination, the constants s1, s2 : State , u' : User and e : Elt are generated. By implication elimination and conjunction elimination, three new equations are introduced in the specification, namely database(s1) = database(s2) , temp-mem(s1) = temp-mem(s2) and U:User (not-ack(U,s1) = not-ack(U,s2)) . Now, there are three subgoals left to prove. The first two, database(ack(u',e,s1)) = database(ack(u',e,s2)) and temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2)) are immediate, but the third, U:User (not-ack(U,ack(u',e,s1)) = not-ack(U,ack(u',e,s2))), requires quantifier elimination. So, a new constant u : User is introduced and the new goal becomes not-ack(u,ack(u',e,s1)) = not-ack(u,ack(u',e,s2)). Because of the operational semantics of the OBJ's _==_ , we need to treat two cases, u == u' or u =\= u' . The rest of the proof is easy now.

A first set of easy behavioral properties which can be proved right now is the idempotency of methodes, i.e., of insert , submit , receive and ack. Why should we be interested in idempotency? This is because the low level daemons use bare IP, so the sender daemon just keep sending messages until acknowledgements are received and the acknowledger daemon just send acknowledges whenever messages are received. So it is very possible to receive or acknowledge many times the same message. On the other way, a user can reinsert or resubmit the same proof either by purpose or by mistake (similar situations appear when the email is used).

All of the following properties are proved relatively similarly, so we discuss only the idempotency of receive in the explanation page. Formally, we need to prove the following (behavioral) first order formula:

F:Elt (S:State (receive(F,receive(F,S)) = receive(F,S)))

Since we have already proved the behavioral coherence of the specification, the simplest way to prove the behavioral property above is to use attribute coinduction. This yields another first order formula, namely:

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))) ) .

As usual, we prove it by firstly eliminating the quantifiers, i.e., by introducing two constants f :Elt and s :State , and then by eliminating the conjunction, so generating three subgoals:

1. database(receive(f,receive(f,s))) = database(receive(f,s)) ,
   
2. temp-mem(receive(f,receive(f,s))) = temp-mem(receive(f,s)) , and
   
3. U:User (not-ack(U,receive(f,receive(f,s))) = not-ack(U,receive(f,s))) .

The first two subgoals follow immediately by reduction, but the third one needs quantifier elimination first and then reduction.

All methods involved are commutative in a special sense, namely, that the order in which the same method is applied (as a consequence of unpredictable external events) in a given state is not important, that is, behavioral equivalent states are obtained. In the case of receive , for example, the following behavioral equality should be proved:

F1,F2:Elt S:State (receive(F1,receive(F2,S)) = receive(F2, receive(F1,S))).

The generated proof is very simple (relatively), but it is highly based on two properties of the left and right closures, namely:

L,R:Set E:Elt (l< l< L, R >, add(E, r< L, R >) > = l< L, add(E,R) >), and
L,R:Set E:Elt (r< l< L, R >, add(E, r< L, R >) > = r< L, add(E,R) >).

We refer the reader to the explanation page of the specification for more information about the closure operations. In principle, these two properties say that it is not necessary to make closures after each added element; it is enough to make only one closure after more elements are added.

Perhaps the most interesting proof on this page is the commutativity of ack. The first order formula which should be proved is:

F1,F2:Elt U1,U2:User S:State (ack(U1,F1,ack(U2,F2,S)) = ack(U2,F2,ack(U1,F1,S))).

What makes this example different from the others is that a case analysis is required. This is because three constants u,u1,u2:User are involved at some point in the proof (these constants are generated by the quantifier elimination rule), and because the special predicate _==_ is used for the sort User in the PROTOCOL specification.

We saw some properties emphisizing the distributed aspect of the tatami protocol in the previous pages. The goal of those properties was to show that receiving or submiting a message twice, or the order in which messages are received from the internet did not affect the state of the system. But all these properties do not say anything about the corectness of the protocol.

But actually, what is the corectness of the protocol? Since all applications can access the state of the protocol using only the three atributes database , temp-mem , and not-ack, we must define the corectness in terms of these attributes. But temp-mem is only an extra facility offered by our system (in the same way in which "mailq" is an extra facility offered to the email users), so the consistency of the elements found there is not guaranteed, and not-ack shows only the communication status with the other users. Therefore, we formulate the correctness of the Tatami Protocol as follows:

For every reachable state S, database(S) is consistent.

Putting all these together, we have to prove the following three first order formulas:

1. ok?(database(init)) = true,
2. S:State F:Elt (ok?(database(S)) = true and ok?(parents(F),database(S)) = true) implies
           (ok?(database(insert(F,S))) = true and ok?(database(insert(F,S))) = true)), and
3. S:State (ok?(database(S)) = true) implies
           F:Elt (ok?(database(receive(F,S))) = true) and
           F:Elt U:User (ok?(database(ack(U,F,S))) = true)).