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

We denote the updating of a map ρ so that i now maps to d by ρ }

The identifer τ is used to denote the clock-tick or clock-cycle count, so it is
best viewed as mapping to an integer—however the associated value and its type
is simply immaterial, as will become apparent later on.
Data items of type Fun do not form part of the state, but are used as a
technical device to capture the fact that expressions in channel output guards
are evaluated when that guard goes “live”, if ever.
Expression evaluation w.r.t an environment is defined in the normal way, and
returns a result of type Datum that is not itself of type Fun :

†{ i → d

E : Exp → Env → Datum

E [[ e ]] ρ = “standard” expression evaluation. . .

Note however, that the partial application [[ e ]] , w h e r e e denotes a value of type

Val , can be interpreted as a Datum value result of (sub-)type Fun .

E

6.2 Static State

The “static state” of a Handel-C program is that part of the state which persists
across clock-cycle boundaries, and its evolution over those time-slots is what
constitutes the observable behaviour of a Handel-C program.
For any Handel-C program, we simply identify all the variables used, in as-
signments, expressions, and channel inputs. We then tailor the environment so
that its domain contains precisely those variables.

6.3 Dynamic State

The dynamic state is that which only exists within one clock cycle, and is effec-
tively “zeroed” at every clock tick. It contains information about communica-
tion requests and is that part of the environment accessed by the identifiers

,γ

and B .
At the start of each clock cycle, these are initialised to be empty:

ρ ( γ )= θ ρ ( B )= ∅ ρ ( )=( θ, ∅ )

6.4 Actions for Handel-C

We want our actions to be state-transformers, that is functions from state to
state, and we need to define the null action ( nop ), as well as explaining how
actions merge (

♦ ).

Actions. Formally our actions are functions mapping environments into envi-
ronments, and the null action is simply the identity function on environments.
However, we want to capture the notion of actions that change part of the state,