**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

*SN*[*FA*_{1}]...[*FA*_{n}]

When the list of fitting arguments *FA*_{1}, ..., *FA*_{n} 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 *FA*_{i} 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** *SM*_{i}

**[CHANGED:]** When *SM*_{i} 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 *Sigma*_{i} given by the parameter specification
*SP*_{i}, the signature *Sigma'*_{i} given by the the corresponding
argument specification, and the symbol mapping *SM* determine a
set of signature morphisms from *Sigma*_{i} 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 *FA*_{i} 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** **{** *SP*_{1} **and**...**and** *SP*_{n} **}** **then** *SP*

**[]** Let *FM* be the morphism yielded by the fitting arguments
*FA*_{1}, ..., *FA*_{n}, 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*[*FA*_{1}]...[*FA*_{n}] 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 *FA*_{i}.
**[]** Each model of an argument *FA*_{i}
**[CHANGED:]** (these are models of *SP'*_{i} reduced by the signature morphism
determined by *SM*_{i})
**[]** is required to be a model of the
corresponding parameter *SP*_{i}, 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** **{** *SP*_{1} **and**...**and** *SP*_{n} **}**

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 cofi-language@brics.dk