Version 0.93 and notes

[Michal.Walicki@ii.uib.no (Michal Walicki)]

1.
 From the names proposed so far, CASL is my definite favourite (ALCOL would
be my second choice).

[Does anyone actually object to CASL?  My only worry about it is that
it looks a bit too close to ASL for comfort - but the pronunciation is
quite different, so I don't think that this matters so much.  BTW,
CASL may also stand for CoFI (rather than just Common) Algebraic
Specification Language. --PDM]

2.
In the proposal to drop the cyclic sections, Peter says

>* The well-formedness conditions on TYPE DEFINITION GROUPS are to be
>  relaxed to allow (or maybe require?) the separate declaration of the
>  sorts being defined.

With the strong reading ("require" rather than "allow") isn't it just
saying that TD (TYPE DEFINITION GROUPS) become sentences? 

[No, I don't think so: a CONSTRUCT always declares a constructor
function, and maybe some selector functions too; an alternative SORT
declares a subsort inclusion.  --PDM]

This would be
consistent with the fact that SG (SORT GENERATION constraints) are already
treated in this way. Also, TD are just special case of SG implying more
implicit axioms. Following the suggestion that sorts of TD must be declared
separately, I think it would be clearer to join the two concepts into one:
to "require" separate sort declarations in both cases and to make TD and SG
into special cases of one concept of abstract syntax (or perhaps to make TD
a special case of SG).

[I think that you are assuming that we can write equations between
terms that denote sorts.  This would require something like "Unified
Algebras" or a truly higher-order framework, I think.  --PDM]

3.
One general remark on the recent note of Michel's on parameterization. I am
not convinced that there are sufficient reasons to introduce the
distinction between specs and specs of formal parameters (and some othe
distinctions - see below).

3.1.
As pointed out earlier, nobody would like to write something like:
        Param-Spec TO ...... instead of  Spec TO .....
when specifying total orders just to ensure that this specification can
later be used as a formal parameter. The distinction

a) between specs and specs of parameters

seems to be needed to distinguish

b) a parameterized specification which has been instantiated 'to the end'
(i.e., by an actual parameter which cannot be further instantiated) from
the ones where further instantiation is possible.

I am not convinced that one needs to make the distinction b) either.

3.2
Basically, since the semantics of parameterized specifications is defined
in the "usual way" (as a model class of a corresponding structured
specification), instantiation amounts to a special (and useful) kind of
refinement - namely, only of the parameter part (and with all the renamings
etc.). We have a STACK[ELEM] and the instance STACK[INT] is its refinement.
If we make the distinction a), and b), we would have to say that this last
specification can be further refined in the usual way, but not by means of
instantiation. Why? If I later come with another INT' spec which is more
refined than INT, why should it be forbidden to make STACK[INT'] from
STACK[INT] in the same way as I made STACK[INT] from STACK[ELEM]? Or else,
why would I have to make STACK[INT'] from STACK[ELEM] and not from
STACK[INT]?

3.3
Another motivation for the distinction a) is that it allows one to 'fix'
parts of the formal parameter and forbid changing them in instantiation
(cf. Michel's example STACK2[NAMED-ELEM]). It should not be difficult to
construct an example where one would have a specification SP with two
things (sorts or functions) A and B, and then wanted to write two different
parameterized specification PA[SP] and PB[SP] in such a way that PA wants
to keep 'fixed' A, while PB wants to keep 'fixed' B. In the current
proposal this would require at least two specifications of the same formal
parameter SP. If this SP is, for instance, a TO which one may need
independently as such, one would also need a third version where it is not
a formal par spec but usual spec.

3.4
This means (at least for me) that even if 'fixed' parts are important, the
distinction a) is not the desirable way to proceed. I think that it would
be much more natural to enforce this kind of 'fixing' at the moment when a
spec SP is being used as a formal parameter, i.e., when writing the
parameterized spec P[SP]. That is, we get a flavour of different 'modes of
parameter passing': in some cases everything remains open, while in other
some parts of formal parameter are identified as 'fixed'.

[Michel is very busy with distributing FASE'97 papers to PC members
these days, so don't hold your breath while waiting for his answer...
Of course, others are welcome to respond to your comments too!  --PDM]

        Michal