Go backward to State Functions and PredicatesGo up to TopGo forward to Predicates as 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