Comments on rationales

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,

here are my comments to the CoFi and the CASL rationales.
I hope that they are not too late. I first read 18th May
as deadline, and now saw that the CASL rationale should
be finalized already on May 15th.

[Sorry, where was the latter?  It must have been a typo, or outdated...
The deadline was indeed 18th May, although I'm only just starting the
preparations of the final versions just now, so comments are still welcome
today! --PDM]

CoFI rationale
--------------

p.8/p.9
The paragraph in the middle of p.8 correctly describes
the current situation, but the foreground on p.9 seems
to be written at some time before, so some items
from p.8 reappear here in a less completed stage
(e.g. on p.9, the semantics group is contemplating
what semantic entities would be needed for a formal
semantics, while on p.8 the formal semantics for
(most of) the tentative design is available.

p.8, 2nd last para:

[Ini97d] is cited, but this is the rationale itself?!


CASL rationale
--------------

p.1:
CASL = CoFI *Algebraic* Specification Language
As Gordon Plotkin pointed out in Edinburgh, it may sound
strange to call a language algebraic if its expressiveness
goes beyond first-order logic. So I propose either to switch
to "Axiomatic" here,

[I'd rather leave such a decision to the IFIP WG 1.3 meeting.  --PDM]

or to explain that keeping "algebraic"
since the approach of "algebraic specification"
started with algebraic methods, which have nice
properties and constructions (initial models and
free extensions) which are still useful, but that we
need to go beyond algebra to full first-order
logic and (second order) induction principles to write
easy-readable specifications and capute all aspects
of computation.

[I'll try to add something along those lines.  --PDM]

p.6, last lines
I find the last sentence a bit cryptic. Which questions
do not have optimal solutions? I think that Kleenes
three valued logic is a logic which is very useful for
capturing aspects of computation, and it is needed
in any case when describing properties of programs.
The point is that we do not introduce it at the level
of specifications to keep the underlying logic easy
and simple, and leave it to the specifier to speciy
three- or more-valued logics when needed for an application.

[OK  --PDM]

p.8, Predicates
"difficult to motivate" is not very precise.
In my opinion, the crucial argument for having predicates
instead of only boolean-valued functions is that
they allow to inductively specify relations,
e.g. the transitive closure of a binary relation.

[Thanks for reminding me of this important point!  --PDM]

p.11, Union and extension
To the first sentence, the possibility of extension
by new subsort relations could be added.

p.12 4.3 Initiality and freeness
... involving disjunction and negation *and existential
quanitifcation*.

At several places (e.g p. 11 botton), CASL is written
 "Casl" when put boldface.

[Apparently small-caps and boldface don't mix so well in LaTeX2e.  This
will cure itself when the boldface disappears in the final versions. --PDM]


Greetings,
Till