VAR-ITEMS ::= var-items VAR-DECL+
A list VAR-ITEMS of variable declarations is written:
vars VD1; ... VDn;
Note that local variable declarations are written in a similar way, but followed directly by a bullet ` · '.
VAR-DECL ::= var-decl VAR+ SORT VAR ::= SIMPLE-ID
A variable declaration VAR-DECL is written:
V1, ..., Vn : s
It declares the variables V1, ..., Vn of sort s for use in subsequent axioms, but it does not contribute to the declared signature.
The scope of a global variable declaration is the subsequent axioms of the enclosing basic specification; a later declaration for a variable with the same identifier overrides the earlier declaration (regardless of whether the sorts of the variables are the same). A global declaration of a variable is equivalent to adding a universal quantification on that variable to the subsequent axioms of the enclosing basic specification.