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 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.
[]