Go backward to The Logic of ActionsGo up to TopGo forward to Actions |

- 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