Go backward to Validity and ProvabilityGo up to TopGo forward to The Enabled Predicate |

- Program described using parameter
`n`.- Mathematician: variable (symbol does not represent known value).
- Programmer: constant (value of
`n`does not change).

- Two kinds of variables:
- Rigid variables (unknown constant).
- (Flexible) variables (program variable).

- Constant expressions:
- Built from rigid variables and constant symbols.
- Extend state functions and actions to contain constant expressions.

- Quantification over rigid variables
*s*[[*exists*`m`in**Nat**:`m`*x'*=`n`+*x*]]*<=>**exists*`m`in**Nat**:`m`(*t*[[*x*]]) =`n`+*s*[[*x*]]`A`is valid if*s*[[`A`]]*t*equals**true**for all states*s,t*and all possible values of its free rigid variables.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998