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 --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Up Next