6 Structuring ConstructsTopII Structured Specifications5 Structuring Concepts

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  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. 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 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 (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. 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 symbol mappings determine signature morphisms as follows:

CoFI Document: CASL/Summary -- Version: 1.0.1 -- 25 March 2001.
Comments to cofi-language@brics.dk

6 Structuring ConstructsTopII Structured Specifications5 Structuring Concepts