Prev Up
Go backward to 2.2.1 Global Variable Declarations
Go up to 2.2 Variables

2.2.2 Local Variable Declarations

      LOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+

A localization LOCAL-VAR-AXIOMS of variable declarations to a list of axioms is written:

vars VD1; ...; VDn · F1 ... · Fm;
The sign displayed as ` · ' may be input as `·' in ISO Latin-1, or as `.' in ASCII.

It declares variables for local use in the axioms F1, ..., Fm, but it does not contribute to the declared signature. A local declaration of a variable is equivalent to adding a universal quantification on that variable to all the indicated axioms.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to

Prev Up