Prev Up Next
Go backward to II Structured Specifications
Go up to Top
Go forward to 6 Structuring Constructs

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--and vice versa. 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 (implicit or 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:


CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Prev Up Next