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
  • s[[exists m in Nat: mx' = 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.