Up Next
Go up to 6.2 Named and Parametrized Specifications
Go forward to 6.2.2 Specification Instantiation

6.2.1 Specification Definitions

      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:

spec
SN [SP1] ... [SPn] given SP"1, ..., SP"m =
SP
end
When the list of imports SP"1, ..., SP"m is empty, the definition is written:
spec
SN [SP1] ... [SPn] =
SP
end
When the list of parameters SP1, ..., SPn is empty, the definition merely names a specification and is simply written:
spec
SN =
SP
end
The terminating `end' keyword is optional.

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

The well-formedness and semantics of a generic specification are essentially as for the imports, extended by the union of the parameter specifications, extended by the body:

{ SP"1 and...and SP"m } then { SP1 and...and SPn } then SP
[CHANGED:] The local environment given to the defined specification is empty, i.e., the above specification is implicitly closed. [] The 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. [CHANGED:] The imports, in contrast, are fixed, and common to the parameters, body, and arguments. [] 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.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Up Next