Re: Proposal for Generic Extensions with Import Clauses

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

Dear Hubert,

We have just had another look at your proposal for generic extensions.

One issue arose: conservativity.

First, you do not mention what is the semantics of

	GEN-CONS-EXT ::= gen-cons-ext IMPORT? PARAMS SPEC+ 

We presume that the conservativity requirement applies here to the
subsequent extensions of PARAMS (by SPEC+), right? 

Another option would be to make this to apply also to the "first
step", ie, to the extension of IMPORT by PARAMS. However, instead of
proposing this, we suggest that perhaps we could consider a more
general solution, where we might have two forms of import, indicating
whether its further extension is required to be conservative or not.

Even though at least one of us (guess who) in general questions the
necessity of the conservativity requirements in structured specs, this
would seem uniform with the way conservativity may be imposed
elsewhere in CASL.

So perhaps we should have:

IMPORT               ::= CONSERVATIVE-IMPORT | JUST-IMPORT
JUST-IMPORT          ::= import SPEC
CONSERVATIVE-IMPORT  ::= conservatively import SPEC

Then there would be no conservativity requirement on the extension of
the import SPEC by PARAMS (either in gen-spec or in gen-cons-spec) for
the JUST-IMPORT clause. If, however, the CONSERVATIVE-IMPORT clause
was used then this would imply that

a) in the generic extension (whether conservative or not), PARAMS
	would have to extend the import SPEC conservatively

b) at each instantiation of this generic spec (whether conservative
	or not), the actual parameters would have to extend the import
	SPEC conservatively as well.

We do not think that any further elaboration (like formal parameters
extend import conservatively but actual parameters need not to, or
vice versa) can be easily justified.

Any reactions?

Best regards,

Michel and Andrzej