A Denotational Semantics for Handel-C - Formal Methods and Hybrid Real-Time Systems - page 56

Unlike the microslot-sequence case, here we do merge slot-sequences from the
front.

5.5 Framework Summary

We have defined a notion of guarded actions, and microslots capturing sequences
of sel , req and res actions, as well as slots which put these before a clock-cycle
terminating action action. We have defined traces as non-empty lists of such
slots, with all but the last slot obliged to have an action action, and defined
trace concatenation ( 9 ) and parallel merge ([][]) operators. Both have monoid
properties, with the null trace as identity, and [][] also being commutative.

6Ex cu onS e

We now turn our attention to the actions of the previous section, and elaborate
how these are in fact state-transformers. To this end, we first need to understand
what is meant by the state of a Handel-C program.

6.1 Environments

We follow the classical approach for imperative languages in that the state is
an “environment”: a mapping from identifiers to values. We differ in that while
some identifiers denote program variables, others have special meaning and cor-
respond to internal processing carried out during a clock-cycle, largely to do
with processing prialt communication requests.
We define identifiers ( Id ) to be either variable names ( Var ) or one of four
special identifiers τ, ,γ or B , not present in Var . We define a value space ( Val )

to contain integers, booleans and an error value (?), and then define a datum
type as being either a value, a function Fun , or one of the three types associated
with prialt resolution, namely Resltn , CPMap and PriSet :

i ∈ Id = Var + { τ, ,γ,B }

Val = Z + B + { ? }

f ∈ Fun = Var → Val

d ∈ Datum = Val + Fun + Resltn + CPMap + PriSet

Although we have used disjoint union or sum above, in the sequel we do not
explicitly show the relevant injections, so that we interpret a value x : as also

being a value x : Val ,oreven x : Datum , rather than writing the more pedantic
but verbose forms of inj 1 ( x ): Val and inj 1 ( inj 1 ( x )) : Datum .
We define an environment ρ as a mapping from identifiers to data, subject to
the proviso that variables map only to values,

Z

maps only to Resltn s, and γ
and B map respectively to the CPMap and PriGrp components of ρ ( ):

ρ ∈ Env = Id → Datum