Information Technology Reference
In-Depth Information
Within this representation,
V
is a vector of variables of types
T
, initialized with
values
I
,all
A
i
stands for non-deterministic,
demonic choice. Demonic choice of actions means that when an aborting action
is enabled, this action is chosen. Notice that after “inline'ning” all imported
functions
(1
≤
i
≤
d
) are actions, and
F
I
,
Z
denotes the set of imported variables of the environment that
was accessed by the imported functions.
After eliminating all function calls, the action system consists of basic actions
only (cf. Table 1) and all actions are part of the
do od
-block, also known as
Dijkstra's guarded iteration statement [6]. The guarded iteration statement can
be thought of as being a loop that selects one enabled action
A
i
for execution in
each iteration. In case there is no action enabled, execution of the action system
ceases as execution of the loop terminates.
We can determine the enabledness of an action
A
i
by computing the enabled-
ness guard: Because we do not want an action
A
i
to be enabled for states in which
it is guaranteed to establish any postcondition, i.e. behave miraculously, the en-
abledness guard is defined as
g.A
=
df
¬
∈
wp
(
A, f alse
), where
wp
:
Action
×
(
State
→
Bool
)
Bool
) is the weakest precondition predicate transformer. For
example, the precondition of a guarded command is given by
→
(
State
→
wp
(requires
guard
:
A
end
,q
)
≡
guard
⇒
wp
(
A
,q
)
with “
” denoting logical implication. Table 1 lists the weakest preconditions
of all actions for any given predicate
q
.
⇒
Table 1.
Semantics of Basic Actions
Action
Notation
wp
(
Action
,q
)
Sequential Composition
S
1
;
...
;
S
n
wp
(
S
1
,wp
(
...,wp
(
S
n
,q
)))
Nondeterministic Composition
S
1
S
2
wp
(
S
1
,q
)
∧ wp
(
S
2
,q
)
Prioritizing Composition
S
1
//S
2
wp
(
S
1
,q
)
∧
(
¬g.S
1
⇒ wp
(
S
2
,q
))
requires
p
:
S
1
end
p ⇒ wp
(
S
1
,q
)
Guarded Command
Multiple Assignment
y
:=
e
q
[
y
:=
e
]
Nondeterministic Assignment
z
:=
z
with
Q
(
∀z
∈ Q.z · q
[
z
:=
z
])
Local Variables
var
∀x
1
...x
n
:
wp
(
S, q
)
x
1
:
T
1
;
...
;
x
n
:
T
n
:
S
Skip
skip
q
Abort
abort
false
In Table 1,
S
1
,S
2
each denote an action,
y
lists of variables,
z, z
variables,
e
is a list of expressions,
p
is a predicate over the state of the action system,
g.S
1
is the enabledness guard of action
S
1
, and Q is a predicate over
z
,
z
(and the
state). The nondeterministic assignment assigns to variable
z
the value of
z
for
which Q holds. The statement aborts if this is not possible [3]. Notice that an
action will terminate if the
termination guard
t.A
=
wp
(
A, true
)holds.
