[CoFI] Removal of conservative extensions from CASL

[Michel.Bidoit@lsv.ens-cachan.fr]

[At the Bremen meetings two weeks ago, Michel indicated that he would
 support the removal of conservative extensions from CASL.  However, we
 did not consider it appropriate for those of us in Bremen to decide on
 this issue during the meetings, since it had not (recently) been
 discussed on this mailing list.  After the meetings, Michel confirmed
 his position on the issue, and has kindly provided the following brief
 rationale.  I've taken the liberty of already removing the keyword
 "conservatively" from the proposed CASL v0.99 concrete syntax and
 examples, and the corresponding construct from the abstract syntax -
 but the issue is open for public discussion, along with the other
 changes.  Please send comments as soon as possible, rather than
 waiting until just before the deadline (Monday 9 February)!  --PDM]


Rationale for removing " conservative extensions " from CASL
============================================================

EXTENSION ::= extension SPEC SPEC+
CONS-EXTN ::= cons-extn SPEC SPEC+

The "conservative" case does not really affect the semantics of the
extension, but can only result in an ill-formed specification. More
precisely, let us consider the following (abstract) example:

SPEC = extension SPEC1 SPEC2
SPECbis = cons-extn SPEC1 SPEC2

We have two cases:

  * Either the extension is indeed conservative, i.e. Mod(SPEC)
reduced to the signature of SPEC1 is exactly equal to Mod(SPEC1). 
In that case, SPECbis is well-formed and its semantics is the same as
the one of SPEC.

  * Or the extension is not conservative, i.e. Mod(SPEC) reduced to
the signature of SPEC1 is strictly included into Mod(SPEC1). In that
case, SPECbis is ill-formed.

Therefore, the use of a "conservative extension" construct instead of
the corresponding "standard extension" merely reflects the "intention"
of the specifier that the corresponding extension is intended to be
conservative.  This means that "conservative" here stands for some
proof obligation.

 From a methodological point of view, I would say that conservative
extensions are not the right concept and are likely to lead to
misunderstandings and bad use of CASL constructs.

First, some CASL users may believe that a conservative extension
"protects" the extended specification. This is not quite true (or
rather not true at all), since there is no obligation for any further
extension to be conservative too. I.e. the specification

SPECter = extension (cons-extn SPEC1 SPEC2) SPEC3

is legal (and well-formed if SPECbis was well-formed) even if SPEC3 is
not a conservative extension of SPECbis, i.e. if Mod(SPECter) reduced
to the signature of SPEC1 is strictly included in Mod(SPEC1).

It is not possible to "protect" a specification SPEC at the level of
structured specifications in CASL; indeed such a "protection" makes no
sense, and it is unfortunate that "conservative extension" conveys a
wrong intuition.

Indeed, CASL provides means for "protecting" parts of a modular system
specification using architectural specifications. The adequate way to
express this is:

unit spec P-SPEC1 = SPEC1

arch spec SYS = 
  units
    M : P-SPEC1
    N : use P-SPEC1 for SPEC2
  result N

As a unit specification, P-SPEC1 "protects" SPEC1: all contexts where
P-SPEC1 will be used are architectural specifications which must
preserve the model class of P-SPEC1 (hence of SPEC1) to be
well-formed.  The point here is that the "protection effect" is
obtained by embedding the structured specification SPEC11 into an
architectural unit specification P-SPEC1.
[Note: this is very similar to what was designed in the PLUSS
specification language.]
[Note: the reasoning above is correct provided there is no coercion
from arch specs to structured specs in CASL, since these coercions
will "remove" the protection barrier.]  
[Such a coercion was indeed proposed in Note M-4, but subsequently
 dropped in the syntax proposed for architectural specifications in
 v0.99.  --PDM] 

Second, so far proof obligations are (rightly) not reflected at the
level of CASL. It is expected that some annotations will be designed
to allow the user for annotating her specifications with proof
obligations (in the style of the implies clause of LSL). It would
therefore be more consistent to remove conservative extension from
CASL, and to provide instead annotations to state that some extensions
are INTENDED to be conservative.

This would altogether simplify the language, and remove opportunities
for the user to misunderstand and misuse the concept.

Note that if it is the case that some tools would be able to use the
fact (or assumption) that a given extension is conservative, it is
even more consistent with the rest of the design of CASL to state the
conservativeness fact/assumption as an annotation, which in general
are provided for that very purpose.

Please react !!!
-- 
Michel Bidoit
Laboratoire Specification et Verification       Tel:  +33 (0)1 47 40 28 68
CNRS URA 2236                                   Secr: +33 (0)1 47 40 24 04
Ecole Normale Superieure de Cachan              Fax:  +33 (0)1 47 40 24 64
61, Avenue du President Wilson		
94235 CACHAN Cedex France                Email: Michel.Bidoit@lsv.ens-cachan.fr