Go backward to Type Definition Group
Go up to Structuring Constructs

Generic Specifications

SPEC-DEFN       ::=   spec-defn SPEC-NAME GEN-SPEC
SPEC-NAME       ::=   SIMPLE-ID
A specification definition SPEC-DEFN provides a name SPEC-NAME for a (possibly generic) specification GEN-SPEC. 

GEN-SPEC        ::=   gen-spec OF-SPEC* SPEC
The abstract syntax of a generic specification GEN-SPEC is similar to those of an EXTENSION: each declared parameter is an OF-SPEC, so persistency may be required by use of a PERSISTENT-SPEC, and freeness of the body SPEC may be specified by use of a FREE-SPEC. The well-formedness and semantics of GEN-SPEC are essentially as for the corresponding EXTENSION, the only difference being that a fitting argument has to be supplied for each declared parameter when referencing a GEN-SPEC through its name, as explained below. A GEN-SPEC with an empty OF-SPEC* list may be regarded as an ordinary, non-generic specification.

N.B. When a declared parameter is merely a SPEC-NAME, it refers to an existing specification definition in the global environment--it is not a local name for an argument specification. A declared parameter, whatever its form, essentially just specifies the signature and sentences that the body of the generic specification may assume to be provided by the corresponding argument specification that is supplied when referencing the generic specification. Thus the parameter specification corresponds more to the type of the argument than to a formal parameter. 

SPEC            ::=   ... | SPEC-INST
SPEC-INST       ::=   spec-inst SPEC-NAME FITTING-ARG* SIG-MORPH?
FITTING-ARG     ::=   fitting-arg SPEC SIG-MORPH?
A specification instantiation SPEC-INST refers to the possibly-generic specification named SPEC-NAME in the global environment, providing a fitting argument FITTING-ARG for each declared parameter (in the same order).

A fitting argument FITTING-ARG fits the argument specification SPEC to the corresponding parameter specification via a signature morphism SIG-MORPH. An omitted SIG-MORPH construct is taken to be the identity morphism.

When there is more than one parameter, the fitting argument morphisms have to be  compatible, with all of them extending to a single morphism, including moreover any fitting morphism SIG-MORPH that is specified as a component of the enclosing SPEC-INST. Thus any common parts of declared parameters have to be instantiated in the same way. It is pointless to declare the same parameter twice in a generic specification. (Generic specifications that require two similar but independent parameters can be expressed by using a translation to distinguish between the symbols in the signatures of the two parameters.)

The semantics of a well-formed instantiation SPEC-INST is the same as that of the specification determined as follows: the fitting morphisms are extended to a single morphism applicable to the signature of the entire generic specification GEN-SPEC named by the SPEC-NAME, any persistency and freeness requirements are checked, then the translation of it by this morphism is united with all the argument specifications. 

ID              ::=   ... | COMPOUND-ID
COMPOUND-ID     ::=   compound-id SIMPLE-ID ID+
This extension of the syntax of identifiers for sorts, functions, and predicates is of relevance to generic specifications. In a compound identifier COMPOUND-ID, the components may (but need not) themselves identify sorts, functions, or predicates that are specified in the declared parameters of a generic specification.

When such a compound identifier is used to name, e.g., a sort in the body of a generic specification, the translation determined by fitting arguments to parameters applies to the components ID+ of the compound identifier as well. Thus instantiations with different arguments generally give rise to different compound identifiers for what would otherwise be the same sort, which avoids unintended identifications when the instantiations are united.

E.g., a generic specification of sequences of arbitrary elements might use the simple identifier Elem for a sort in the parameter, and a compound identifier compound-id Seq Elem for the sort of sequences in the body. Fitting various argument sorts to Elem in different instantiations then results in distinct sorts of sequences.

Subsort embeddings between component sorts induce subsort embeddings between the compound sorts. For example, when Nat is declared as a subsort of Int, we get automatically (compound-id Seq Nat) embedded as a subsort of (compound-id Seq Int) in signatures containing all these sorts.

The details of the intended relationship between compound identifiers and other constructs (such as translations and reductions) have still to be decided. Higher-order extensions of CASL are expected to provide a more semantic treatment of parametrized sorts, etc.

CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk