The local environment for each named specification is fixed,
consisting only of the pre-declared signature (the constant predicates
true and false).
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
[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.
CoFI
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk