The local environment for each named specification is fixed,
consisting only of the pre-declared signature (the constant predicates
true and false). 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.
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
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk