2.2.1 Global Variable Declarations

      VAR-ITEMS ::= var-items VAR-DECL+

A list VAR-ITEMS of variable declarations is written:

vars VD₁; ... VD_n;

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:

V₁, ..., V_n : s

It declares the variables V₁, ..., V_n 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.