5 Structuring Concepts |

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

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.
^{8}

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

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

A named specification may declare some ** parameters**, the
union of which is extended by a

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. For the semantics of structured specifications (in particular, those involving hiding) the axiom of choice is assumed.

The semantics of views involves also ** specification
morphisms**, which are signature morphisms between particular
specifications such that the reduct of each model of the target
specification is a model of the source specification.

Given a signature *Sigma* with symbols *|Sigma|*, ** symbol
sets** and

- 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 names in*|Sigma|*. In the case that the signature morphism does not exist, the enclosing construct is ill-formed. - Given another signature
*Sigma'*, a mapping of symbols in*|Sigma|*to symbols in*|Sigma'|*determines the unique signature morphism from*Sigma*to*Sigma'*that extends the given mapping, and then is the identity, as far as possible, on common names of*Sigma*and*Sigma'*. (Mapping an operation or predicate symbol implies mapping the sorts in the profile consistently.) In the case that the signature morphism does not exist or is not unique, the enclosing construct is ill-formed.

CoFI Document: CASL/Summary -- Version: 1.0.1 -- 25 March 2001.

Comments to cofi-language@brics.dk

5 Structuring Concepts |