SPEC-DEFN ::= spec-defn SPEC-NAME GENERICITY SPEC GENERICITY ::= genericity PARAMS IMPORTS PARAMS ::= params SPEC* IMPORTS ::= imports SPEC*
A generic specification definition SPEC-DEFN with some parameters and some imports is written:
When the list of imports SP"1, ..., SP"m is empty, the definition is written:
- spec
- SN [SP1] ... [SPn] given SP"1, ..., SP"m =
- SP
- end
When the list of parameters SP1, ..., SPn is empty, the definition merely names a specification and is simply written:
- spec
- SN [SP1] ... [SPn] =
- SP
- end
The terminating `end' keyword is optional.
- spec
- SN =
- SP
- end
It defines the name SN to refer to the specification that has parameter specifications SP1, ..., SPn (if any), import specifications SP"1, ..., SP"m (if any), and body specification SP. This extends the global environment (which must not already include a definition for SN). The local environment given to the defined specification is empty, i.e., the specification is implicitly closed. The well-formedness and semantics of a generic specification are essentially as for the union of the parameter specifications and the imports, extended by the body:
{ SP1 and ... and SPn and SP"1 and ... and SP"m } then SPThe difference between declaring parameters and leaving them implicit in an extension is that each parameter has to be provided with a fitting argument specification in all references to the specification name SN. The declared parameters show just which parts of the generic specification are intended to vary between different references to it.
N.B. When a declared parameter happens to be merely a specification name, it always must refer to an existing specification definition in the global environment--it does not declare a local name for an argument specification.
SPEC-NAME ::= SIMPLE-ID
A specification name SPEC-NAME is normally displayed in a SMALL-CAPS font, and input in mixed upper and lower case.