Go backward to
The Logic of Actions
Go up to
Top
Go forward to
Actions
State Functions and Predicates
State function
Expression built from variables and constant symbols.
s
[[
x
2
+y-3
]] = (
s
[[
x
]])
2
+
s
[[
y
]]-3.
s
[[
f
]] :=
f
(
forall
'
v
':
s
[[
v
]]/
v
)
Correspond to program expressions (and subexpressions of assertions).
State predicate
Boolean expression.
x
2
= y-3
s
[[
P
]] in {
true
,
false
}.
s
satisfies
P
iff
s
[[
P
]] =
true
.
Correspond to assertions (and boolean-valued program expressions).
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998