Prev Up
Go backward to 6.2.1 Specification Definitions
Go up to 6.2 Named and Parametrized Specifications

6.2.2 Specification Instantiation

      SPEC      ::= ... | SPEC-INST
      SPEC-INST ::= spec-inst SPEC-NAME FIT-ARG*

An instantiation SPEC-INST of a generic specification with some fitting argument specifications is written

When the list of fitting arguments FA1, ..., FAn is empty, the instantiation is merely a reference to the name of a specification that has no declared parameters at all, and it is simply written `SN'. Note that the grouping braces `{ }', normally required when writing free (or closed) specifications, may always be omitted around instantiations.

The instantiation refers to the specification named SN in the global environment, providing a fitting argument FAi for each declared parameter (in the same order).

      FIT-ARG  ::= FIT-SPEC
      FIT-SPEC ::= fit-spec SPEC SYMB-MAP-ITEMS* 

A fitting argument specification FIT-SPEC is written:

SP'i fit SMi
[CHANGED:] When SMi is empty, the fitting argument specification is simply written SP'i. Symbol mappings SM are described in Sections 6.4 and 6.5. [] The signature Sigmai given by the parameter specification SPi, the signature Sigma'i given by the the corresponding argument specification, and the symbol mapping SM determine a set of signature morphisms from Sigmai to Sigma'i, as explained in Chapter 5. The fitting argument is well-formed only when this set is a singleton, i.e., the fitting argument morphism is well-defined. Note that mapping an operation or predicate symbol generally implies non-identity mapping of the sorts in the profile.

When there is more than one parameter, the separate fitting argument morphisms have to be  compatible, and their union has to yield a single morphism from the union of the parameters to the union of the arguments. Thus any common parts of declared parameters have to be instantiated in the same way, and 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.)

[CHANGED:] Each fitting argument FAi is regarded as an extension of the union of the imports and the current local environment. The fitting argument morphism has to be identity on all symbols declared by the imports SP"1, ..., SP"m of the generic specification, if there are any.

Let SP' be the extension of the imports by the generic parameters and then by the body of the specification named SN:

{ SP"1 and...and SP"m } then { SP1 and...and SPn } then SP
[] Let FM be the morphism yielded by the fitting arguments FA1, ..., FAn, extended to a morphism applicable to the signature of SP' [CHANGED:] as explained in Sections 6.4 and 6.5 [] (and written as a list of symbol maps). Then the semantics of the well-formed instantiation SN[FA1]...[FAn] is the same as that of the specification: [CHANGED:]
{ SP' with FM } and SP'1 and...and SP'n
where each SP'i is the specification of the corresponding fitting argument FAi. []
Each model of an argument FAi [CHANGED:] (these are models of SP'i reduced by the signature morphism determined by SMi) [] is required to be a model of the corresponding parameter SPi, otherwise the instantiation is undefined. The instantiation is also undefined whenever the [CHANGED:] result signature is not a push-out of the body and argument signatures: if the translated body
{ SP' with FM }
and the actual parameter
SP'1 and...and SP'n
share any symbols, these symbols have to be translations (along FM) of symbols that share in the extension of the imports by the generic parameters
{ SP"1 and...and SP"m } then { SP1 and...and SPn }
Here, two sorts share if they are identical, and two function or predicate symbols share if they are in the overloading relation. []

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to

Prev Up