next up previous
Next: Semantics for the model Up: Semantical Aspects of an Previous: Structure of this paper


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


next up previous
Next: Semantics for the model Up: Semantical Aspects of an Previous: Structure of this paper
Roel Bloo 1999-11-26