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

it occurs ( sel , req , res , act ), with an assertion that indicates the conditions under
which that action (and all subsequent) may proceed.
This switch also brings the semantics more in line with that of Circus [30]
and its slotted variants [31], fitting in with plans to give a complete account of
Handel-C and hardware compilation in the UTP framework [32].

5.1 Abstraction of Action, States and Predicates

We shall now present an abstract view of typed assertion traces, where actions
( a : Act ) with an action merge operator ♦ form a commutative monoid, with

the “null” action nop as identity.

Mon ( Act , ♦ , nop )

We the introduce an abstract notion of a state ( s St ) as something which can

change as a result of actions, and denote the effect of action a on state s by

∈

[ a ]( s ). The null action, not unexpectedly, brings about no change of state:

: Act → St → St [ nop ]( s )= s

We need predicates over states (assertions), with true and false denoting the
everywhere true and false predicates respectively:

p ∈ Pred = St → B

We are going to capture the linkage between assertions and actions by the con-
cept of a “guarded-action” ( g ), which is a predicate-action pair ( p, e ):

g, ( p, a ) ∈ GA = Pred × Act

We will frequently deal with cases where either the guard is true or the action
is nop , so we adopt the shorthands where a denotes ( true, a )and p denotes
( p, nop ). In particular we often refer to true as a null or void action.
We can extend the notion of action-merging to guarded actions in the obvious
way by merging the actions and taking the conjunction of the predicates:

( p 1 , a 1 ) ♦ ( p 2 , a 2 ) =( p 1 ∧ p 2 , a 1 ♦ a 2 )

These guarded actions are the basic building blocks for “assertion traces”, so
the next step is to describe the typing aspects.

5.2 Typed Assertion Traces

We shall view a trace as being a non-empty sequence of slots, were each slot
denotes the activity during one complete clock cycle. We allow traces to be
either finite or infinite, as this is required for the semantics of any of the loop
constructs.

Trc = Slot ∗ ∪ Slot ω τ ∈