SPEC ::= BASIC-SPEC | TRANSLATION | REDUCTION
| UNION | EXTENSION | FREE-SPEC | LOCAL-SPEC
| CLOSED-SPEC
A translation allows the symbols declared by a specification to be renamed; it may also be used to require that some symbols have been declared, e.g., when referencing a named specification. A reduction allows symbols to be hidden; for convenience, the remaining `revealed' symbols may be simultaneously renamed. A union combines specifications such that when the declaration of a particular symbol is common to some of the combined specifications, its interpretation in a model has to be a common one too. An extension may enrich models by declaring new symbols and asserting their properties, and/or specialize the interpretation of already-declared symbols. A free specification FREE-SPEC is used to restrict interpretations to free extensions, with initiality as a special case. A local specification LOCAL-SPEC is used to specify auxiliary symbols for local use, hiding them afterwards. A closed specification CLOSED-SPEC ensures that the local environment provided to a specification is empty.
When the above constructs are combined in the same specification, the grouping is determined unambiguously by precedence rules: translations and reductions have the highest precedence, then come local specifications, then unions, and finally extensions have the lowest precedence. (Free specifications generally involve explicit grouping, and their relative precedence to the other constructs is irrelevant.) A different grouping may always be obtained by use of grouping braces: `{ ... }'.
A specification SPEC may occur in a context (e.g., when it being named) where it is required to be self-contained or closed, not depending on the local environment at all. In that case, it determines a signature and a class of models straightforwardly.
In structured specifications, however, a specification SPEC may also occur in a context where it is to extend other specifications, providing itself only part of a signature. Then it is interpreted as a (partial) function mapping signatures Sigma to the corresponding extended signatures Sigma', together with a partial function mapping model classes over Sigma to model classes over Sigma' (when defined). The signature and model class for the self-contained case above can be obtained by applying these functions to the empty signature and to the model class of the empty specification, respectively.
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.