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.
LIB-NAME ::= LIB-ID | LIB-VERSION LIB-VERSION ::= lib-version LIB-ID VERSION VERSION ::= version NUMBER+
A library identifier LIB-ID in a local library may be written as a simple identifier. A library version name LIB-VERSION in a local library is written:
LI version N1. ... .NnThe lists of version numbers are ordered lexicographically on the basis of the usual ordering between natural numbers.