Syntax of a Splice-like coordination language

To high-light the essential ideas, we incorporate the basic Splice interaction primitives in a simple imperative coordination language.

With respect to the questions listed in section 1.2 the following choices have been made. Queries are predicates on data items and a state, the read operation returns exactly one data item satisfying the query and blocks if there is none. The question whether the set of available data items is the same for all consumers at any time corresponds to the choice between the global or the local model.

We assume a data type ${\tt Data}$ and a set of variables ${\tt Vars}$. Then the state of a program is a function from variables to data, i.e., ${\tt States}= {\tt Vars}\rightarrow {\tt Data}$, and expressions are functions of type ${\tt States}\rightarrow {\tt Data}$. Now programs in our language are defined as follows:

$$\begin{eqnarray*} P & ::= & {\tt Skip}~\mid~{\tt Write}(e)~\mid~{\tt Read}(x, q... ...&~\mid~P_1 ~;~P_2~\mid~P_1 ~\vert\vert~P_2~\mid~{\tt Close}(P). \end{eqnarray*}$$

Some remarks are in order here:

• ${\tt Skip}$ denotes the empty program.
• ${\tt Write}(e)$ writes the data value denoted by expression $e$ to the dataspace.
• ${\tt Read}(x, q)$ assigns to the variable $x$ a previously written data element satisfying the query $q$. It blocks if there is no such element.
• $P_1 ~;~P_2$ denotes sequential composition.
• $P_1 ~\vert\vert~P_2$ denotes parallel composition. As a syntactic constraint, we require that the set of variables of the two processes in the parallel composition be disjoint.
• ${\tt Close}( P )$ denotes the closure operation. It specifies that all data items that have been read by statements in $P$ also have been produced by preceding writes inside $P$. There is no hiding of the produced data items, so they might be read by an external reader.

In PVS, this language is represented as an abstract datatype, which allows us to use recursive definitions and proofs by induction on the structure of programs.

Note that, for simplicity, we do not distinguish between different datasorts. An extension to multiple sorts and adding a sort to the closure operation, is straightforward. Similarly, it is easy to add more programming constructs such as assignment, choice, and while. See, for instance, [7] for the denotational semantics of a real-time imperative programming language in PVS.