comments on CASL Tutorial

[Giuseppe Scollo <scollo@arena.sci.univr.it>]

Dear Michel and Peter,

  My Software Engineering lectures are over for this term,
so now I could find the time to give you a few comments
and feedback about your CASL Tutorial. Generally I found
it very useful, for it allowed me to introduce algebraic
specification to third-year students in a learn-by-example
manner, which was quite effective. Actually, I had to
spend a couple of lectures on basic concepts of algebraic
specification first, since the tutorial assumes such a
background right from the start. For the rest, the examples
are fairly clear, and are very useful in pointing out a
few semantic issues which would not be evident otherwise,
especially for a "strict-algebraic" (no predicates) mindset.

  So, here are my remarks and questions. Almost all of them
are of fairly minor relevance, except for the first question,
which really puzzled me and my students. I'd appreciate your
reaction to this question first, even if separately from
any reaction to the other remarks below.

  Best regards,
                Pippo

[I will try to answer Pippo's points asap. Michel]

-------------------------------------------------------------

Example on p. 77. [A case of "parametric inconsistency"?]

  The parameter of this specification is the PARTIAL_ORDER spec,
which is the second spec on p. 10, I assume. It then turns out
that some instances of LIST_WITH_ORDER_2 [...] have no model.
These are precisely those instances where the partial order is
not total, since no 

 order : List --> List

may ever yield a permutation of the argument list such that
the is_sorted predicate holds on it. 

  Now, the question is what do you want to show by this example.
If your purpose is that of illustrating that one may write
parametrically inconsistent specifications in CASL, that's a
good example. Perhaps you would rather formulate this unusual
concept by saying that the specification violates the semantics
of the parameter, in the sense that it unduly restricts its
model class. However, one expects a different purpose, viz. an
illustration of the use of local specification. Then I should
suggest to replace the given parameter with a specification of
(reflexive-transitive) total orders. A similar replacement would
be in place for the example on p. 76, of course.

Examples on pp. 9-10. [Terminology]

  Your terminology as of the examples on pp. 9-10 leads one to
refer to a reflexive-transitive total order as a "total partial order", which is not wrong but sounds strange. As an alternative
you may consider to call "strict total order" what you call just
"total order" on p. 10, whereas "total order" would refer to
reflexive-transitive total orders. Thus one gets:
   partial order = strict partial order + Id
   total order = strict total order + Id
where "+" means extension and "Id" is the identity relation.

Example on p. 9. [Superfluous axiom, noted by student M. Sabadini]

  The second axiom is an easy consequence of the other two axioms,
thus either you had better take it out or you take this chance to
introduce the "%implies" annotation (example on p. 11).

Example on p. 25. [Superfluous variable]

  The variable "y" is not made use of in the equations.

Example on p. 26. [Question]

  Perhaps replacing "Predicates" with "Ground predicates" would
yield a more accurate statement?

Example on p. 31. [Question]

  Is the third axiom necessary? I should not expect so, after the
statement on p. 26: "Predicates hold minimally in models of free
specifications", but perhaps the difference is made by the fact
that here we have a free extension of a (loose) parameter spec.,
rather than simply a free spec.; how's the matter?

Example on p. 37. [Remark]

  The example is very useful, in that it shows that "free" is not
synonym of "freely generated"; however, it also contradicts the
belief that "free specifications provide initial semantics" (p. 23)
in all cases. Perhaps something like "(when initial models exist)"
should be inserted in the statement on p. 23.

Example on p. 43. [Remark]

  The example thus implies that (strong) equality is not at all an
ordinary predicate, in that it may hold on undefined arguments;
perhaps this should be pointed out.

Example on p. 63. [Arithmetic]

  The number 1 is not prime (there are good reasons for this), thus
the factor "1 < x" should be added to the defining axiom for sort
Prime.

_____________
Dr. G. Scollo, University of Verona, DST, Software Engineering
scollo@arena.sci.univr.it    http://arena.sci.univr.it/~scollo