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
SN[FA1]...[FAn]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 SMiWhen 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 corresponding argument specification, and the symbol mapping SM determine a signature morphism from Sigmai to Sigma'i, as explained in Chapter 5. The fitting argument is well-formed only when the signature morphism is defined, 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.)
Each fitting argument FAi is regarded as an extension of the union of the imports (the current local environment is ignored). 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 SPLet FM be the morphism yielded by the fitting arguments FA1, ..., FAn, extended to a morphism applicable to the signature of SP' 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:
{ SP' with FM } and SP'1 and...and SP'nwhere each SP'i is the specification of the corresponding fitting argument FAi. Each model of an argument FAi (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 not well-formed if the result signature is not a push-out of the body and argument signatures: if the translated body
{ SP' with FM }and the union of the argument specifications
SP'1 and...and SP'nshare 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.