Go backward to
State Functions and Predicates
Go up to
Top
Go forward to
Predicates as Actions
Actions
Action
= boolean-valued expression.
Variables, primed variables, constant symbols.
x'+y = y
,
x-1
in
z'
.
Relation between
old
state and
new
state.
Unprimed variables refer to old state.
Primed variables refer to new state.
Representation of atomic operation of concurrent program.
Formalization of
A
[[
A
]] in
St
->
S
->
Bool
s
[[
A
]]
t
in
Bool
.
Old state
s
, new state
t
.
s
[[
A
]]
t
<=>
A
(
forall
'
v
:
s
[[
v
]]/
v
,
t
[[
v
]]/
v'
).
s
[[
y = x'+1
]]
t
= (
s
[[
y
]] =
t
[[
x
]]+1).
s,t
is an
A
step
iff
s
[[
A
]]
t
=
true
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998