! LIB-DEFN ::= lib-defn LIB-NAME LIB-ITEM* ! LIB-ITEM ::= SPEC-DEFN | VIEW-DEFN ! | ARCH-SPEC-DEFN | UNIT-SPEC-DEFN
A library definition LIB-DEFN is (tentatively!) written:
library LN LI1... LIn
It provides a collection of specification (and perhaps also view) definitions. It is well-formed only when the defined names are distinct, and not referenced until (strictly) after their definitions. The global environment for each definition is that determined by the preceding definitions. Thus a library in CASL provides linear visibility, and mutual or cyclic chains of references are not allowed.
The local environment for each named specification is empty: the symbols declared by the preceding specifications in the library are made available by explicit reference to the name of the specification concerned--possibly using the require construct of structured specifications to indicate which symbols come from which specifications.
Each specification defined by a library must be self-contained (after resolving references to names defined in the current global environment), determining a complete signature--fragments of specifications cannot be named.
A local library definition determines a libary name, together with a map from names to the semantics of the named specifications.