5.3 Static Semantics

5.3.1 PAR-TYPE

5.3.2 Definition

Let us denote by FN_i (for Free Names) the generic symbols of the ith-parameter type, that is the symbols of the signature of Spⁱ that do not appear in the signature of any Spⁱ_j.

Then, such declaration is well-formed in an environment if each Par_i is well-formed and moreover the following conditions hold:

Coherence

Symbols in any FN_i cannot belong to the fixed part of other parameters. Notice that the signatures of different parameters are not required to be disjoint; indeed the intersection of the generic parts of the signatures of different parameters may be non-empty, as well as the intersection of their fixed parts. In particular, several parameters with the same PAR-TYPE are allowed.

No double declarations

Each parameter name can occur at the most once in the list of formal parameters of a generic spec, as usual.

Sp_Body

Symbols in the signature of any parameter cannot be redeclared in the body Sp_Body.

The body of a generic spec has to be well formed in the current environment enriched by the parameter names, that are assumed to have the signatures described by the corresponding qualifying specs Spⁱ.

Moreover, the body must be unambiguous. Following the principle that generic symbols are just place holders, such symbols cannot be confused with generic symbols declared (with the same profile, if it is a function or a predicate) in the qualifying specification of some other parameter. Thus, if a symbol name (with the same profile, if it is a function or a predicate) belongs to FN_i and FN_j for i/=j, then it must be referred to using its source as well as its name.

This requires the following changes to the abstract syntax as well

SORT      ::= ... | referenced-sort SORT-NAME SPEC-NAME
FUN-NAME  ::= ... | referenced-fun FUN-NAME SPEC-NAME
PRED-NAME ::= ... | referenced-pred PRED-NAME SPEC-NAME

where the referenced constructs is well formed only within the body of a generic specification with the SPEC-NAME part corresponding to the name of (one of) the formal parameters, whose signature includes in its varying part that symbol name.

The body of a generic spec can be any kind of expression not only an extension of a union (as in the current proposal), but notice that if the parameters have to be (persistently) extended, then this has to be explicitly stated in the body.

5.3.3 Instantiation

An instantiation is statically correct iff acceptable fitting parameters are provided for all formal parameters (in the same order).

An acceptable fitting parameter corresponding to a formal parameter of type par-type Sp^i fixed-names Sp^i_1...Sp^i_k^i consists of

• a specification Sp^A (the actual parameter) over a signature Sigma^A and, possibly
• a list sigma= sig-morph simb-map alpha_1 alpha'_1... simb-map alpha_n alpha'_n where sigma is a consistent renaming of generic symbols from FNⁱ into Sigma^A and the symbols not mapped by sigma belongs (with the correct profile, if needed) to Sigma^A as well. That is the alpha_j are all distinct², each alpha_j belongs to FNⁱ and by adding the identity association for all other symbols in the signature of Spⁱ but the alpha_j's we get a signature morphism from signature of Spⁱ into Sigma^A.

---

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