some more fixes and questions

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

Hi,

  The exercise of running through the same CASL tutorial examples
at the second edition of my SE course was fruitful again. Please
find enclosed a couple of new bugfixes, comments and questions.

  Regards,
           Pippo

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

Further comments on CASL Tutorial by M. Bidoit & P. D. Mosses
    made after its use in the Software Engineering Course
    at University of Verona, DST, september-november 2000

                       Giuseppe Scollo


Example on p. 77. [One more fix, one more question]

  In addition to the correction suggested in my previous comments(*)
on this example, another one seems in place. The definition of
the local predicate "same_elements" entails its validity iff its
argument lists have the same underlying *sets* of elements. Then
its use in the axiom for the "order" operation has the questionable
effect of allowing models where this operation returns a list that
differs from the argument list not only for the order of element
occurrences but also for the multiplicity of their occurrences.

  The obvious fix consists in replacing "same_elements" with a
binary predicate that should be specified to hold iff its argument
lists have the same underlying *multisets* of elements. Then also
the membership predicate "is_in" should be replaced, by a binary
operation yielding the number of occurrences of the given element
in the given list. This is fairly easy to specify, but the fix
raises the following question about localization.

  Is localization limited to (newly declared) signature symbols and
related axioms, or is it also allowed for imports, by reference to
a specification? That is to say, in the subject example, may one
refer to a "NATURAL_n" spec just within the "local" part of the
example? 


Examples on p. 84-85. [Question]

  The example are allright, but do not tell whether, or exemplify
how, name clashes are avoided in parameterized instantiations.
Would the following be OK?

   spec LIST_OF_LIST [sort Elem] =
        LIST_5 [LIST_5 fit Elem |-> List[Elem] ]
   end


Example on p. 49. [Superfluous variable]

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

________
(*) URL: http://arena.sci.univr.it/~scollo/ids2000/lab/doc/casl/Comments.txt

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