[CoFI] Re: DRAFT Response to Referee Report on CASL

[Don Sannella <dts@dcs.ed.ac.uk>]

Here are my reactions to the draft response to the CASL referee
report.  I agree with everything that I don't mention explicitly
below.

2.1: At present, the structuring part isn't institution-independent.
We could try to make it more institution-independent, with a big step
in this direction being to drop compound identifiers.  I wouldn't mind
this change -- these seem to introduce more problems than any other
feature of CASL.

2.1, 2.2, 3.2.1 et al: Whether we change the design or not, I agree
that we should emphasize the institutional structure more than we have
done.  I have already added the required things to the semantics of
basic specs for CASL v0.97 (CoFI Semantics note S-6, to appear soon).

2.3: I only semi-agree with the first half of the suggested response.
First, I don't believe that there are so many existing specifications
in other languages that translating them automatically to CASL is
really a priority.  Second, demonstrating embeddability of a language
X in CASL is a proof that users of X could become users of CASL
without sacrificing anything, and even in the absence of existing
specs in X that could be a useful thing.

3.1.1: If the changes to CASL that are required to address the empty
carrier issue are not very minor, I would be against making them on
the grounds that the practical advantages of allowing empty carriers
are very small if any.

3.1.2: In the semantics, existential equality is considered as basic
with strong equality as an abbreviation.  Similarly, implication is
the only basic connective with conjunction, disjunction, negation, and
equivalence as abbreviations.

Giving the semantics of CASL via definition of a kernel sub-language
is not a bad idea.  But we didn't start that way so adopting this
approach would be considerable extra work that we can't afford now.

3.2.1: I don't know what exactly the referees are referring to in
point 2 (structural properties of CASL semantics; taking profit from
the well-developed structural theory of algebraic specifications).  I
can try to guess but I'm not sure what they had in mind.

In the response, I'm not sure what exactly is meant by "the
compositionality of the `natural style semantics'", especially if this
is something that isn't already well-known concerning this style of
semantics.

3.2.2: I'm not sure what exactly "the categorical aspects of the given
semantics" refers to.

3.2.3: I see no chance that we will be able to find resources for this
additional level of semantics without a funded project.

3.3.1: It might be worth mentioning in the response that the ideas
behind architectural specifications and the distinction between these
and generics are not new, but go back at least to a paper by myself,
Sokolowski and Tarlecki in Acta Informatica 29:689--736 (1992).  So
while these ideas aren't as widely known as some others on which CASL
is based, they aren't exactly half-baked.

Best regards, Don

___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner    courier mail only:
FB3 Mathematik und Informatik      MZH 8071, FB3
Universitaet Bremen                Universitaet Bremen
Postfach 330 440                   Bibliothekstr. 1
D-28334 Bremen                     D-28359 Bremen

Telefon: (+49) 421-218-3660        telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE       privat:  (+49) 421-25-1024
NEW: http://www.informatik.uni-bremen.de/~bkb