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:
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.)