Related work

Since our aim is to develop a compositional proof system for proving properties about Splice programs, we defined a denotational semantics for the Splice interaction primitives. There are already a few other semantic models for closely related languages. We discuss the operational semantics of [3,4] and an algebraic framework [5].

In [3] a transition system semantics for a subset of Splice interaction primitives is presented. The resulting semantics is similar to our implementation model semantics. Differences are the use of a new operation to fork processes instead of parallel composition, a get operation and the absence of a state so that write operations can only write values. The queries are predicates on data only.

In [4], Bonsangue et al. study the relationship between several different models for a data-oriented coordination language. Although we do not have an explicit database in the semantics, it is possible to construct one corresponding to each semantic primitive. Then our conceptual model corresponds to the unordered centralized system with a set dataspace in [4], and our implementation model is related to their distributed system with a set dataspace. Bonsangue et al. show that these two systems are equivalent for programs using read, write and test-for-absence operators. Apart from the fact that we give a denotational semantics where Bonsangue et al. give an operational semantics and that our semantics and proofs have been formalized in PVS, a difference between their work and ours is that read operations do not have queries in [4]. Simple queries on the requested data item only can be simulated in the system of Bonsangue by using a (possibly infinite) choice, but we allow stronger queries, namely on the current state as well as the data value. These queries can not be simulated in the system of Bonsangue et al. This explains why in [4] the systems are equivalent even in the presence of a test-for-absence.

Another approach for giving a semantics to part of the Splice language has been taken in [5], where Splice is described in terms of process algebraic laws. The approach is inspired by a process algebra for describing delay-insensitive communications. Whereas the aim of [5] is to be able to reason and compute algebraically with programs, we aim at compositional assertional verification of programs. Indeed we can prove properties formally that have are axiomatized as laws in the Splice Process Algebra of [5]. A few examples of general process algebraic laws that have been proven to hold in our semantics:

• Symmetry of $~\vert\vert~$, i.e., $\mbox{$[\![\:$}P_1 ~\vert\vert~P_2\mbox{$\:]\!]$} = \mbox{$[\![\:$}P_2 ~\vert\vert~P_1\mbox{$\:]\!]$}$ for all programs $P_1, P_2$.
• Associativity of $~\vert\vert~$ and $~;~$, that is, for all programs $P_1, P_2, P_3$, $\mbox{$[\![\:$}P_1 ~\vert\vert~(P_2 ~\vert\vert~P_3)\mbox{$\:]\!]$} = \mbox{$[\![\:$}(P_1 ~\vert\vert~P_2) ~\vert\vert~P_3\mbox{$\:]\!]$}$
  and $\mbox{$[\![\:$}P_1 ~;~(P_2 ~;~P_3)\mbox{$\:]\!]$} = \mbox{$[\![\:$}(P_1 ~;~P_2) ~;~P_3\mbox{$\:]\!]$}$.

The following general law has also been proven.

• Sequential composition of write statements is equivalent to their parallel composition:
  $\mbox{$[\![\:$}{\tt Write}(e_1) ~;~{\tt Write}(e_2)\mbox{$\:]\!]$}$ = $\mbox{$[\![\:$}{\tt Write}(e_1) ~\vert\vert~{\tt Write}(e_2)\mbox{$\:]\!]$}$, for all expressions $e_1, e_2$.

Now we have, as a consequence of the first and third law above, law 10 from [5] (we translate the action-prefix of the Splice process algebra to sequential composition):

• Symmetry of sequential writes:

  $\mbox{$[\![\:$}{\tt Write}(e_1) ~;~{\tt Write}(e_2)\mbox{$\:]\!]$} = \mbox{$[\![\:$}{\tt Write}(e_2) ~;~{\tt Write}(e_1)\mbox{$\:]\!]$}$, again for all expressions $e_1, e_2$,