Prev Up Next
Go backward to 3.4 Variable Declarations
Go up to 3 Basic Specifications
Go forward to 3.6 Attributions

3.5 Visibility and Scope

The order in which items of basic specifications are listed is insignficant.
Basic specifications in CASL involve items of various syntactic categories: signature declarations (sorts, subsorts, functions, predicates, datatypes), variable declarations, attributions, axioms, and sort generation constraints.

In many cases, it is possible to group these items in a natural order: first sort and subsort declarations, then function and predicate declarations, etc., and finally the axioms) with each item referring only to the symbols declared in the preceding items. However, it may also be desirable to group axioms together with the sorts, functions, and predicates that they define, or to defer the declarations and axioms concerning auxiliary entities (to be hidden) to the end of the list. Moreover, datatype declarations may often be best presented in a `top-down' order (cf. the grammar for the abstract syntax of CASL); they may also involve `mutual recursion' that cannot be linearized at all (unless extra declarations of sorts are inserted).

Such considerations motivated the CASL design decision to allow items of basic specifications to be listed in any order. Thus parsers (human or otherwise) for CASL have to take account of the entire enclosing basic specification regarding declarations of the symbols used in each item. On the other hand, they do not have to keep track of a varying local environment, reflecting the scopes of declarations within basic specifications.

Note that the structured specifications of CASL do allow linear visibility to be expressed: by means of a list of extensions, where each step of extension might even be essentially a single declaration or axiom (but note that the scopes of variable declarations are limited to the list of basic items in which they occur). And the specification of auxiliary entities may be separated as a local specification, which corresponds to a combination of extension and hiding.


CoFI Document: CASL/Rationale --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk

Prev Up Next