2 Our Proposal in a Nut Shell

the name

of the generic specification;

the list of its parameters

each of them consists of a specification name, that occurs once in the list, and its type.

The typing is given by a specification, describing the overall signature of the parameter and the relevant properties of its interpretation, and a set of "symbol-fixing" specifications, whose signatures represent the symbols that cannot be renamed by any instantiation. The symbols of the overall specification that do not appear in any symbol-fixing specification are called "generic".

Generic symbols of one parameter cannot be fixed symbols of other parameters, but the signatures of different parameters are not required to be disjoint and, in particular, several parameters with the same type are allowed.

the body

that is an expression of type SPEC well-formed in the current environment enriched by the formal parameters assumed to have the signature described by their typing.

Generic symbols cannot be redeclared in the body and the body must be unambiguous, that is a generic symbol declared in two or more paramaters must be referred to using its source as well as its name. This requires the add a new construct for sorts, function and predicate names to allow them to be qualified by a specification name.

GEN-SPEC    ::= gen-spec PAR+ SPEC

PAR         ::= par SPEC-NAME+ PAR-TYPE
PAR-TYPE    ::= par-type SPEC FIXED-SYMB?
FIXED-SYMB ::= fixed-symb SPEC+

The abstract syntax of a generic specification instantiation requires

the name

of the generic specification;

arguments

each of them consisting of a specification (the actual parameter) and a fitting morphism, translating the generic symbols to corresponding symbols of the signature of the actual parameter.

GEN-SPEC-INST::= gen-spec-inst GEN-SPEC-NAME FITTING-ARG+
FITTING-ARG ::= fitting-arg SPEC SIG-MORPH?

A generic specification instantiation is statically correct if its actual parameters are given in the correct order and each fitting morphism yields a signature morphism from the signature of the formal to that of the actual parameter when completed by the identity on the fixed symbols.

A generic specification instantiation is dynamically correct if the translation of each actual parameter along the corresponding fitting morphism is a subset of the model class of the corresponding formal parameter.¹

Notice that no conditions of coherence between the fitting morphisms corresponding to different parameters are required, as only the "generic" symbols are translated and such may be interpreted by different elements.

The semantics of a generic specification instantiation is the semantics of its body, where all the "generic" names have been replaced by the actual names provided by the fitting morphisms, evaluated in the current environment where the formal parameters have been associated with the corresponding actual parameter.

---

CoFI Note: L-3 --DRAFT, Version 0.2-- 21 May 1997.
Comments to cerioli@disi.unige.it