1 Why to change?

We agree that named parameters are not needed in the current proposal and that such proposal is sound and coherent, but we also find it not as convenient to use, and especially to explain to non-experts, as more standard approaches would be.

Indeed, even if names would not be needed at all, we believe that it would be convenient to have them, in order to have a syntax closer to the standard ones in programming languages (as well as in mathematical theories). This, in our experience, proves to be a great improvement for acceptance of formal methods by practitioners.

Moreover, though having two parameters of the same kind maybe not so usual (but for instance it happens for pairs, relations, maps, records,...), in such cases the parameter type has to be duplicated in the current proposal in order to be used.

It is worth noting that the "standard" functional style we are advocating makes the treatment of generics conceptually and semantically independent w.r.t. the decisions made for the other constructs. Indeed, such approach is compatible with any language whose expressions have a formally defined evaluation in an environment where the name of the formal parameters may be bound to actual specifications.

Another advantage of the classic functional style is that adopting it we could simplify some constructs that in the current proposal are so strong for generics to be sufficiently expressive. Indeed, the name of the formal parameter can be omitted in the current proposal just because the parameters are used in a silent and fixed way in the body of the specification, that is they are implicitly extended. But there are many examples where the parameters are not used only as starting specifications to be extended adding new symbols and their properties, but in more sophisticated ways. Thus the extend construct has to be sufficiently powerful to somehow simulate all the other constructs. This is, in our opinion, the main reason for allowing the extending part to be an arbitrary specification. That, in turn, introduces the following two problems.

Complex semantics

Using an arbitrary SPEC to extend anotherone, requires SPEC to represent specification fragments instead of self-contained specifications. Therefore the semantics of a SPEC must be a function instead than simply a pair consisting of its signature and model class.

Referential transparency

Since a SPEC may be used to extend another one, we have the problems pointed out by Andrzej and Hubert on referential transparency, that, if we correctly understood, entails that the semantics of an expression using a named specification may differ from the semantics of the same expression where the expression describing the semantics of the name has been substituted for the name, even if the expression describing the semantics of the name is closed (self-contained).

We regard this point as very relevant from a methodological point of view. Indeed, this is strongly counter-intuitive and we expect it to be very hard to explain to our end-users.

Finally, we think that our proposal allows what we believe a methodological improvement, that is to classify the (minimal) syntax of the parameters into "fixed" and "generic". Indeed, in many examples we have "fixed" symbols, that are those imported from already defined basic specifications, like the signature for natural numbers or booleans. Hence, the fixed names should not be touched by the fitting morphisms, while there is no way to impose it in the current language.

On the other hand, we have "generic" sorts (and functions an predicates), that are those that are just place holders, in the sense that they are expected to be replaced by many different actual structures, like the sort elem in the parameters for list, set...
Thus, such signature elements do not have a "reasonable name" and any naming discipline would suggest to have a uniform notation for them; this situation is the same as for indexes of loops in programming languages, that should have meaningless names, exactly to suggest their nature. For instance, all such sorts could be called srt (with a progressive index, if there are many in the same parameter) to help the user to remember that they may be any sort.
But, if there are several parameters this criterion leads to the sharing of the symbols that happen to have the same name (due to the uniformity of naming) in different parameters, while intuitively they are not at all related. Notice the difference between this situation and the corresponding concept for architectural specifications. Indeed, in the case of architectural specs, the units (parameters) are expected to represent subsystems and hence names in their signatures are not place holders, but "concrete" objects, that must satisfy the "same name = same thing" principle. On the contrary, in generic specifications the same principle is misleading, and force the users to remember the otherwise uninteresting names used to represent generic objects, in order to avoid clashes.