A basic specification, as described in
Part I, consists essentially of a
signature *Sigma* (declaring symbols) and a set of sentences (axioms
or constraints) over *Sigma*. The semantics of a well-formed basic
specification is the specified signature *Sigma* together with the
class of all *Sigma*-models that satisfy the specified sentences.

A *structured specification* is formed by combining
specifications in various ways, starting from basic specifications.
For instance, specifications may be *united*; a
specification may be *extended* with further signature items
and/or sentences; parts of a signature may be *hidden*; the
signature may be *translated* to use different symbols (with
corresponding translation of the sentences) by a signature morphism;
and models may be restricted to *initial* models.
The abstract syntax of constructs in the CASL language for
presenting such structured specifications is described in
Chapter 6.

The structuring concepts and constructs and their semantics do not
depend on a specific framework of basic specifications. This means
that Part I of the CASL language
design is orthogonal to Part II (and
also to Parts III
and IV). Therefore, CASL basic
specifications as given in Part I can be
restricted to sublanguages or extended in various ways without the
need to reconsider or to change
Parts II,
III,
and IV.
**[CHANGED:]** ^{}6
**[]**

The semantics of a well-formed structured specification is of the same
form as that of a basic specification: a signature *Sigma* together
with a class of *Sigma*-models. Thus the structure of a
specification is *not* reflected in its models: it is used only
to present the specification in a modular style. (Specification of
the *architecture* of models in the CoFI framework is addressed
in Part III.)

Within a structured specification, the *current signature*
may vary. For instance, when two specifications are united, the
signature valid in the one is generally different from that valid in
the other. The association between symbols and their declarations as
given by the valid signature is called the *local environment*.

Parts of structured specifications, in contrast to arbitrary parts of
basic specifications, are potentially reusable--either verbatim, or
with the adjustment of some *parameters*. Specifications
may be *named*, so that the reuse of a specification may be
replaced by a *reference* to it through its name. (Libraries of
named specifications are explained in
Part IV.) The current association
between names and the specifications that they reference is called the
*global environment*.
Named specifications are implicitly *closed*, not depending
on a local environment of declared symbols. A reference to the name
of a specification is equivalent to the referenced specification
itself, provided that the closedness is explicitly ensured.

A named specification may declare some *parameters*, the
union of which is extended by a *body*; it is then called
*generic*. A reference to a generic specification should
*instantiate* it by providing, for each parameter, an
*argument specification* together with a *fitting
morphism* from the parameter to the argument specification.
Fitting may also be achieved by
**[CHANGED:]** (explicit)
**[]** use of named
*views* between the parameter and argument specifications.
The union of the arguments, together with the translation of the
generic specification by an expansion of the fitting morphism,
corresponds to a so-called push-out construction--taking into account
any explicit *imports* of the generic specification, which
allow symbols used in the body to be declared also by arguments.

The semantics of structured specifications involve signature morphisms and the corresponding reducts on models. For instance, hiding some symbols in a specification corresponds to a signature morphism that injects the non-hidden symbols into the original signature; the models, after hiding the symbols, are the reducts of the original models along this morphism. Translation goes the other way: the reducts of models over the translated signature back along the morphism give the original models.

Given a signature *Sigma* with symbols *|Sigma|*, *symbol
sets* and *symbol mappings* determine signature morphisms as
follows:

- A set of symbols in
*|Sigma|*determines the inclusion of the*smallest*subsignature of*Sigma*that contains these symbols. (When an operation or predicate symbol is included, all the sorts in its profile have to be included too.)It also determines the inclusion of the

*largest*subsignature of*Sigma*that does not contain any of these symbols. (When a sort is not included, no operation or predicate symbol with that sort in its profile can be included either.) - A mapping of symbols in
*|Sigma|*determines the morphism from*Sigma*that extends this mapping with identity maps for all the remaining symbols in*|Sigma|*. - Given another signature
*Sigma'*, a mapping of symbols in*|Sigma|*to symbols in*|Sigma'|*determines the set of all morphisms from*Sigma*to*Sigma'*that**[CHANGED:]**extend the given mapping, and then are identity, as far as possible, on common symbols of*Sigma*and*Sigma'*.**[]**(Mapping an operation or predicate symbol implies mapping the sorts in the profile consistently.)

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk