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 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 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. Such ways of combining specifications are independent of the details of the particular institution underlying basic specifications (so they can be applied to subsorted specifications just as well as to many-sorted specifications). The abstract syntax of constructs in the CASL language for presenting such structured specifications is described in the next section.
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 more than in a basic specification. 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. The pre-declared symbols (such as the constant predicates true and false) are always in the local environment, and may not be hidden or renamed.
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.
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 that have some declared parameters are called generic. A reference to a generic specification should provide, for each parameter, an argument specification that instantiates it via a so-called fitting morphism. Under suitable restrictions, 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.