Up Next
Go up to 10 Library Constructs
Go forward to 10.2 Downloading

10.1 Libraries

LIBRARY         ::=   library LIBRARY-ITEM*
LIBRARY-ITEM    ::=   SPEC-DEFN | ARCH-SPEC-DEFN | UNIT-SPEC-DEFN
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.

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.


CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk

Up Next