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 SMiSymbol mappings SM are described in Section 6.4.
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.)
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 generic parameters and imports by the body of the specification named SN:
{ SP1 and ... and SPn and SP"1 and ... and SP"m } then SPLet FM be the morphism yielded by the fitting arguments FA1, ..., FAn, extended to a morphism applicable to the signature of SP' (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"nEach model of an argument FAi is required to be a model of the corresponding parameter SPi, otherwise the instantiation is undefined. The instantiation is also undefined whenever the result is not a push-out.