Up Next
Go up to 2.2 Variables
Go forward to 2.2.2 Local Variable Declarations

2.2.1 Global Variable Declarations

      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.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Up Next