Information Technology Reference
In-Depth Information
A program state is a mapping from a finite set of
program variables
X
de
=
{
to a set of
values
V
.Wewrite
S
de
=
X
V
for the set of pro-
gram states over
X
,
v
for a generic value in
V
,and
s
for a generic program state
in
S
. Our only assumption on
V
is that it contains the boolean values
true
and
false
(in the examples
V
contains also the set of the natural numbers).
The programming language we consider is a simplified variant of Dijkstra's
language of the guarded commands [10] in the style of Chandy and Misra's
UNITY [6]. Henceforth,
P
indicates the set of the possible programs, and
p
a
generic program in
P
. A program is a set of guarded assignments
g
(
x
0
,...,x
n
)
x
0
,...,x
n
}
→
→
x
0
,...,x
n
:=
f
(
x
0
,...,x
n
), where
f
and
g
(the
guard
)are
expressions
over
program variables. We write
E
for the set of the possible expressions. If we
abstract from the notation, a guarded assignment can be considered as the pair
of the expressions (
f, g
). Therefore,
p
is a subset of
E
2
(
p
⊆
E
2
)and
P
is the
powerset of (
E
2
)(
P
de
=
(
E
2
)). We make no assumptions on
E
.
A program executes by selecting a statement among all the statements whose
guards evaluates to
true
in the current state, and executing its assignment. This
process is repeated until all the guards evaluate to
false
(possibly diverging). We
formally define this by assuming the existence of suitable evaluation functions
P
, yielding the values assumed by
f
and
g
in a state. We abstract
from the concrete evaluation procedures. We only assume that the evaluation
of
f
in a state yields another state, and the evaluation of
g
in a state yields
either
true
or
false
—formally,
f
and
g
f
:
S
→
S
and
g
:
S
→{
true, f alse
}
.When
s
=
true
we say that (
f, g
)is
enabled
by
s
. We now define the
single-step
operational semantics
of a program
p
,
g
p
⊆
S
×
p
×
S
, as follows:
(
s,
(
f, g
)
,s
)
s
=
true
and
s
=
∈
p
iff
g
f
s.
(
f,g
)
−−−→
,and
s
p
s
instead of (
s,
(
f, g
)
,s
)
s
to mean that
We write
s
∈
p
→
(
f,g
)
−−−→
s
for some (
f, g
)
s
p
(we also drop the
p
subscript when the program
that we are considering is evident from the context). The one-step operational
semantics of a program defines a labelled transition system whose states are
program states, whose labels are statements, and whose labelled transitions con-
nect states with the effects of the guarded commands on them. The reflective
∈
and transitive closure of the semantic function,
p
∗
, associates each state
s
with all its successors in an arbitrary number of states. These states are said to
be the
reachable
state space of
p
starting from
s
.
The programming language we are considering differs from most mainstream
imperative programming languages in that it does not have control flow state-
ments such as conditionals, loops and sequencing. This is not a limit because
control flow can be encoded explicitly by introducing a program variable
l
which
stores the current location in the program. Figure 1 exemplifies how a C program
is translated to an equivalent one in the guarded command language.
→
Search WWH ::
Custom Search