However, a SPEC 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 partial function mapping signatures to the corresponding extended signatures, and a function mapping model classes over those former signatures for which the signature extension is defined to model classes over the extended signatures. Note that translations and reductions in a SPEC are not allowed to affect symbols that are already in the local environment that is being extended. The other structuring constructs generalize straightforwardly from self-contained specifications to extensions.

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. When a translation is applied to an extension, it must not affect the symbols already declared in the local environment.

  SIG-MORPH        ::=  sig-morph SYMB-MAP*
! SYMB-MAP         ::=  symb-map SYMB SYMB
  SYMB             ::=  SORT | FUN-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, and the second symbol of the map is of the same syntactic category. 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

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. When a reduction is applied to an extension, it must not affect the symbols already declared in the local environment.

Unions and Extensions

  UNION            ::=  union SPEC+

The signature of a UNION is obtained by the ordinary union of the signatures of each SPEC (not the disjoint union). Thus all (non-localized) occurrences of a symbol in the SPECs are interpreted uniformly, rather than being regarded as homonyms for potentially different entities. The models are those whose reduct along each of the signature inclusion morphisms is a model of the respective SPEC.

! EXTENSION        ::=  extension CONSERVATISM? SPEC+
! CONSERVATISM     ::=  conservative

An EXTENSION allows a list of specification extensions SPEC+ with further signature items and sentences. The extensions start from the first SPEC in the list, and proceed stepwise.

When the EXTENSION is conservative, the reducts of the models at each step of the EXTENSION, along the corresponding signature inclusion, must give the same class of models as that determined by the previous step; otherwise, the EXTENSION is deemed to be inconsistent.

The first SPEC in an EXTENSION gets the current local environment; each subsequent SPEC gets its extension by the preceding SPECs.

  FREE-SPEC        ::=  free-spec SPEC

A FREE-SPEC gives the free extension determined by the component SPEC, relative to the current local environment. When the current local environment is empty, this corresponds to restricting the class of models to initial models.

! LOCAL-SPEC       ::=  local-spec SPEC SPEC

A local specification LOCAL-SPEC allows the localization of the specification of auxiliary items in its first SPEC, so that they are only available in the second SPEC. The intended interpretation is as for an extension (in the same order) except that all the symbols declared by the first SPEC (and not already in the local environment that it receives) are then hidden.

---

CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk