Go backward to Validity and Provability
Go up to Top
Go forward to The Enabled Predicate
Rigid Variables and Quantifiers
- 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
- [[exists m in Nat: m =
n+]]
exists m in Nat: m([[]]) =
n+[[]]
- A is valid if [[A]] equals true for all
states and all possible values of its free rigid variables.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine