Go up to Structuring Constructs
Go forward to Type Definition Group

Structured Specifications

SPEC            ::=   BASIC-SPEC | TRANSLATION | REDUCTION
                |     UNION | EXTENSION | FREE-SPEC | TYPE-DEFN-GROUP
A structured specification SPEC may occur in a context where it is required to be  self-contained, depending at most on the pre-declared symbols in the local environment (see the previous section for an explanation of the concept of environment used here). In that case, it determines a signature and a class of models straightforwardly. However, it may also occur in a context where it is supposed to  extend other specifications, providing itself only part of a signature. Then it is interpreted as a function mapping signatures to the corresponding extended signatures, and from model classes over the former signatures to model classes over the extended signatures.

Translations and Reductions

TRANSLATION     ::=   translation SPEC SIG-MORPH
A translation is well-formed when the signature morphism construct SIG-MORPH expands to a signature morphism applicable to the signature of the component specification SPEC. The translation determines the signature obtained by applying the signature morphism, and the class of models consisting exactly of those models whose reducts along the morphism are among those of SPEC. 

SIG-MORPH       ::=   sig-morph SYMB-MAP*
SYMB-MAP        ::=   SORT-MAP | FUN-SYMB-MAP | PRED-SYMB-MAP
SORT-MAP        ::=   sort-map SORT SORT
FUN-SYMB-MAP    ::=   fun-symb-map FUN-SYMB FUN-SYMB
PRED-SYMB-MAP   ::=   pred-symb-map PRED-SYMB PRED-SYMB
A signature morphism construct SIG-MORPH expands to a signature morphism applicable to a particular signature when each first component of a map in the list SYMB-MAP* is a symbol from that signature. Moreover, the union of the maps has to yield a function. Overloaded function symbols FUN-SYMB and predicate symbols PRED-SYMB may be disambiguated by explicit types; when no explicit type is given in a first component of a map SYMB-MAP, all function or predicate symbols with the same name are mapped uniformly. 

REDUCTION       ::=   reduction RESTRICTION SPEC 
RESTRICTION     ::=   restriction EXPOSURE SYMB+
EXPOSURE        ::=   hiding | revealing
SYMB            ::=   SORT | FUN-SYMB | PRED-SYMB
A REDUCTION is well-formed when the set of symbols determined by the RESTRICTION is a subset of the symbols declared in the signature of the component specification SPEC. In the case that the specified EXPOSURE is hiding, it determines the largest sub-signature of the signature of the component specification that does not contain these symbols (note that removing a sort entails removing all the functions and predicate symbols whose declared type involves that sort). In the case that the EXPOSURE is revealing, it determines the smallest sub-signature that does contain the indicated symbols (so revealing a function or predicate symbol entails revealing the sorts involved in its declared type). In both cases, the subsort embedding relation is inherited from that declared by SPEC, and the determined class of models is given by the reducts of the models of the component specification SPEC along the inclusion of the sub-signature determined by the RESTRICTION.

Unions and Extensions

UNION           ::=   union SPEC+
A UNION of several specifications abbreviates their joint (non-persistent) extension by an empty specification. The signature is obtained by the ordinary union of the signatures of each SPEC (not the disjoint union). The models are those whose reduct along each of the signature inclusion morphisms is a model of the respective SPEC. 

EXTENSION       ::=   extension OF-SPEC* SPEC
OF-SPEC         ::=   PERSISTENT-SPEC | SPEC
PERSISTENT-SPEC ::=   persistent-spec SPEC
An EXTENSION allows the extension of the union of some specifications with further signature and sentences. For each PERSISTENT-SPEC used as an OF-SPEC, the reducts of the models of the EXTENSION along the corresponding signature inclusion must give the same class of models as that determined by the SPEC of the PERSISTENT-SPEC, otherwise the EXTENSION is deemed to be inconsistent.

All the OF-SPECs in an EXTENSION get the current local environment; the component SPEC gets moreover all the symbols declared by the OF-SPECs. 

FREE-SPEC       ::=   free-spec SPEC
By using a FREE-SPEC as the component SPEC of an EXTENSION, the class of models is that given by the free extension. When a FREE-SPEC is used other than in an extension, it abbreviates the free extension of an empty OF-SPEC list, which restricts the models to the initial models of the component specification.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk