Information Technology Reference
In-Depth Information
(
, y
→
f
)
,
(
((
b
)
, true, true
)
, x
→
e
)
becomes
{
y
→
f
}‡
b,
{
x
→
e
}
Assignment, Conditional and Sequential Composition.
If we follow an
assignment by a conditional as follows:
x
:=
y
+
z
;
y
:=
z
(
x >
0)
z
:=
y
then calculating this through with the semantics gives:
[[
x
:=
y
+
z
;
y
:=
z
(
x >
0)
z
:=
y
]]
=
{{
x
→
y
+
z
}‡
x >
0
,
{
y
→
z
}
,
} }
We see clearly the same starting action in both traces, and then a choice based
on the sign of
x
guarding the subsequent behaviour, each covered by one of the
two traces.
{
x
→
y
+
z
}‡
x
≤
0
,
{
z
→
y
Parallel Assignment.
We can swap two variables in one clock cycle:
[[
x
:=
y
y
:=
x
]] =
{{
x
→
y, y
→
x
}}
This works because the expressions are evaluated first during the clock cycle,
and the variables are updated simultaneously as the clock ticks. However, if
we attempt to simultaneously assign two different values to one variable, the
semantics flags this as an error
[[
x
:=
e
1
x
:=
e
2
]] =
{{
x
→
?
}}
While Loop.
If we consider a simply busy waiting loop (
b
will hopefully even-
tually be set by some other process), then we calculate the semantics as:
1
]] =
F
i
[[
b
∗
{
{
nils
}|
i
∈
N
}
where
F
(
L
)=
{¬
b
}∪
((
b,
‡
)::
L
))
Evaluating this leads to the result that the set of traces are of the form:
[[
b
∗
1
]] =
{¬
b
,
b,
‡
;
¬
b
,
b,
‡
;
b,
‡
;
¬
b
,
.
b,
‡
;
...
;
b,
‡
;
¬
b
,
i
−
1times
.
b,
‡
;
...
;
b,
‡
...
}
∞
times
Search WWH ::
Custom Search