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 written:
library LN LI1...LInEach library item LIi starts with a distinctive keyword, and may be terminated by an optional `end'.
The library definition 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 definition is empty: the symbols declared by the preceding specifications in the library are only made available by explicit reference to the name of the specification concerned.
Each specification definition in 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 library name, together with a map from names to the semantics of the named specifications.