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$ ²+y-3]] = ( $s$ [[ $x$ ]])²+ $s$ [[ $y$ ]]-3.
- $s$ [[ $f$ ]] := $f$ (forall ' $v$ ': $s$ [[ $v$ ]]/ $v$ )
- Correspond to program expressions (and subexpressions of assertions).
State predicate
- Boolean expression.
- $x$ ² = y-3
- $s$ [[ $P$ ]] in {true, false}.
- $s$ satisfies $P$ iff $s$ [[ $P$ ]] = true.
- Correspond to assertions (and boolean-valued program expressions).

Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine