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

We can now describe the semantics of all constructs except prialt in a
straightforward manner as follows,

[[ ]] : Prog →P Trc

[[ 0 ]] = { nils }

[[ 1 ]] = {‡}

[[ x := e ]] = { ( , { x → e } ) }

[[ p ; q ]] = p ]]

9 [[ q ]]

[[ p q ]] = p ]] [][] [[ q ]]

[[ p b q ]] =( b :: sel [[ p ]] ) ∪ ( ¬ b :: sel [[ q ]] )

[[ b ∗ p ]] = fix L •{ mk sel ( ¬ b ) } ∪ ( b :: sel ([[ p ]]

9 L ))

o

0 , 1 and assignment have a single singleton trace as semantics, being respectively
the empty, clock-tick and single-variable update slots. Sequential and parallel
composition simply combine all their traces with the appropriate trace operator.
The conditional construct prefixes the traces of the “then” outcome with the
condition as a guard predicate, while the traces of the “else” outcome have the
negation of that predicate prefixed instead. It is with this construct that multiple
traces are introduced, and were we ensure that the exclusivity and exhaustiveness
healthiness conditions are met. The while-loop is given a fixpoint semantics, as
is standard for such constructs. In effect it either immediately terminates, if the
guard is false, or else the guard is true, and it then behaves like the loop-body
sequentially composed with the loop itself. Just like the conditional construct,
it also ensures the exclusivity and exhaustiveness criteria are met.

7.1 Extending the Language

The semantics of prialt is best given by breaking the construct down into
simpler components, which mainly correspond to the various phases in which
prialt is active,namely req , res and act .Wenowintroducesomeextensionto
the language to facilitate this —note that these extensions exists solely in order
to elucidate the semantics, and are not available for general use by the Handel-C
programmer.
We extend the expression syntax to include three special forms — a prialt -
waiting predicate ( w g i ), an active guard expression ( a g i ), and a channel data

expression ( δ ( c )):

e ∈ Exp = ... | w g i | a g i | δ ( c )

The waiting predicate takes a prialt -request (guard-list) as argument, and re-
turns true if resolution has determined that that prialt is blocked. It is evalu-
ated, after the req phase, by looking at the B component of the state:

E [[ w g i ]] ρ = g i ∈ ρ ( B )