Information Technology Reference
In-Depth Information
input ports to value assignments for the assigned variables. We shall, however,
take a more general approach which will be useful when we consider parallel
composition:
p
denotes a function on
consistent value assignments
.
An assignment
σ
is
consistent
wrt. a single assignment program
p
, if for every
equation
x
=
e
in
eqs
p
,wehavethat
E
[[
x
]]
σ
=
E
[[
e
]]
σ
,when
x
and
e
are both
defined for
σ
.
The idea behind the semantics of
p
is simple: extend a value assignment by one
iteration through the equations and add a binding for every assigned variable,
where a value has been computed. This process is repeated until no further
binding is obtained. The number of iterations needed is bounded by the depth
of the dependency graph for
p
.
This idea is formalized by two function:
I
[[
eqs
p
]]
∈
VA
→
VA
P
[[
p
]]
∈
VA
→
VA ,
where we assume that
σ
is consistent with
p
in
[[
p
]]
σ
. The func-
tions are defined below such that they preserve this consistency.
The function
I
[[
eqs
p
]]
σ
and
P
I
is defined as follows:
I
{}
]]
σ
[[
=[]
=
[]
if
x
∈
dom
σ
or
E
[[
e
]]
σ
=
⊥
I
[[
{
x
=
e
}
]]
σ
[
x
→E
[[
e
]]
σ
]oth rw e
I
[[
{
x
1
=
e
1
,...,x
n
=
e
n
}
]]
σ
=
I
[[
{
x
1
=
e
1
}
]]
σ
+
···
+
I
[[
{
x
n
=
e
n
}
]]
σ,
where + is the override function on maps. Observe that the resulting value as-
signment is consistent because the
x
1
,x
2
,...,x
n
are mutually distinct variables.
The function
P
is defined by:
i
=0
I
d
[[
eqs
p
]]
i
σ,
P
[[
p
]]
σ
=
where
d
is the depth of the dependency graph for
p
and
g
j
(
x
) denotes the
j
-fold
iteration of the function
g
, i.e.
g
0
(
x
)=
x
and
g
j
+1
(
x
)=
g
(
g
j
(
x
)).
If we order the equations
eqs
p
into a sequence according to the dependency
graph
≺
p
,sothat
x
=
e
1
comes before
y
=
e
2
whenever
y
depends on
x
, i.e.
x
≺
p
y
, then one iteration through the equations will suce, as the dependency
graph is acyclic.
For every well-formed action (
an,p
), let
an
denote the function
P
[[
p
]] . Fu r -
thermore, a consistent set of actions
as
denotes the function
as
=
P
[[
as
]] , w h i c h
is defined element-wise by:
P
[[
as
]]
σ
=
an
a
(
σ
)+
···
+
an
k
(
σ
)
,
for
as
=
{
an
a
,...an
k
}
.
Search WWH ::
Custom Search