Information Technology Reference
In-Depth Information
Pred
=
Exp,
boolean-valued
e
(
ρ
)
=
E
[[
e
]]
ρ
6.5
Fixpoints
We define an ordering
on traces, with
τ
1
τ
2
if
τ
1
is a prefix of
τ
2
.Wenote
that
if all the
traces are prefixes of some single (longest) trace, which is the shortest possible
such trace. For typed assertion traces we say that
τ
1
nils
τ
for any
τ
. A set of traces has a least upper bound w.r.t
τ
2
if there exists
τ
3
such
that
τ
1
9
τ
3
=
τ
2
.
We extend this to an ordering
over sets of traces by saying that
S
1
S
2
if for every
τ
1
in
S
1
there is a
τ
2
in
S
2
such that
τ
1
τ
2
. The least element in
. Again a notion of least upper bound (
)can
this ordering is the set
{
nils
}
be defined w.r.t
.
Our semantic domain is therefore one of trace-sets, ordered by
,andour
semantic definitions produce directed sets. We therefore handle recursion by
taking the least fixed point w.r.t
, and we can compute this as
F
(
L
)=
i∈
N
F
i
fix
L
•
{
{
nils
}}
7
Handel-C Denotational Semantics
We are now in a position to give the denotational semantics of Handel-C. First we
need to introduce some shorthands to manage the complexity of the resulting
expressions. Given a binary operator
over values
s
and
t
of some type we
assume the obvious extensions to act between sets
S
and
T
over the type, or
between elements and sets as follows:
∗
S
∗
T
=
{
s
∗
t
|
s
∈
S
∧
t
∈
T
}
s
∗
T
=
{
s
∗
t
|
t
∈
T
}
The semantics of a Handel-C process is given as a set of typed assertion traces,
subject to the following healthiness conditions: (1)
Traces are maximal:
if a
trace is present, then none of its proper prefixes are; (2)
Mutual Exclusivity:
if
two traces differ, then the pair of guarded actions which first distinguish them
must have mutually exclusive predicates, i.e ones that are never true in the
same environment (3)
Exhaustivness:
given all traces in the set with a common
prefix, then all the guard predicates of the distinguishing actions must exhaust all
possibilities, ie. for any environment, at least one (and only one) will return true.
Conditions (2) and (3) are weakened slightly when we consider the semantics of
prialt
later on.
Search WWH ::
Custom Search