A LIBRARY provides a collection of specification definitions, possibly of various kinds. It is well-formed only when each SPEC-NAME that occurs in the LIBRARY is uniquely defined, and not referenced until (strictly) after its definition. The global environment for each named specification is that determined by the preceding definitions. Thus a LIBRARY here provides linear visibility, and mutual or cyclic chains of references are not allowed.LIBRARY ::= library LIBRARY-ITEM* LIBRARY-ITEM ::= SPEC-DEFN | ARCH-SPEC-DEFN | UNIT-SPEC-DEFN
The local environment for each named specification is fixed, consisting only of the pre-declared signature (the constant predicates true and false).
[AT] true and false are not predicates, they are simply language constructs (see a preceding section).
Discharged: Adjust wording.Each SPEC defined by a library must be self-contained, determining a complete signature after resolving references to names defined in the current global environment--fragments of specifications cannot be named.
A LIBRARY determines a map from names to the semantics of the named specifications.