Re: CASL - Basic Datatypes

[Michel Bidoit <bidoit@lsv.ens-cachan.fr>]

Dear Markus,

I tried to have a quick look to the new version of the Basic Datatypes.
I am not sure that my remarks are of interest to others, so I leave to you
the decision to post this on cofi-language or not.

[Markus agreed to post it.  N.B. The DEADLINE FOR COMMENTS IS TOMORROW!
 See the original message from Markus, appended.  -- PDM]

Some comments on NAT:

1. I suggest to use display annotations for <= and >= in order to
increase the legibility. Otherwise I would prefer leq and geq.

2. What is the purpose of the unary +__ and of abs ? I don't see the
need for these operations at the level of natural numbers ?

3. Similarly, quot seems to be just an alias for div ? Why do we need
two operations ?

4. Obvious typo in Nat_greater_def axiom.

5. From a methodological point of view, I believe it would be better to
   make the definition domains of the partial operations more explicit
   earlier. To relegate these to an implies part is fine from an internal
   validation point of view, but for an external user of the spec, I
   believe that is is important to see "in a glance":
   a) The arity of the operation b) Its definition domain if it is partial
   c) The axioms that defines it d) when appropriate, further properties,
   possibly in an implies part.
   But of course this is matter of taste.

Other comments:

I have lost track of the rationale for distinguishing between the
ExtSpec and the RichSpec. I am afraid I was never convinced by this,
but perhaps I have misunderstood some rationale behind this
idea. Could you please elaborate a bit on this issue (sorry if you
have already explained this to me, I am afraid I have forgotten your
point).

Let consider ExtPartialOrder [PartialOrder]:
* What is the aim of Sigorder ?
* Is your use of SN = %def SPEC and SPEC2 legal ? What is the expected
  meaning ? Does % def apply to {SPEC and SPEC2} or just SPEC ? What is the
  rationale behind ?

* My rationale is that any spec extending (without a non-trivial parameter
  instantiation) a parametrized spec should again be a parametrized spec.
  Thus, if I have SN [ sort elem] = ...
  and then SN2 = SN [sort elem] then ...
  I would rather write SN2 [sort elem] = SN [sort elem] then ...
  This seems not to be the case in the above ExtPartialOrder ?

Best regards,
Michel

ORIGINAL MESSAGE:

From: Markus Roggenbach <roba@tzi.de>
To: cofi-language@brics.dk
Subject: CASL - Basic Datatypes
Date: Thu, 10 May 2001 14:20:15 +0200 (MET DST)

Dear friends,

since the new version of the Basic Datatypes has not been read
by all people due to technical reasons, please now have a look at
 
http://www.informatik.uni-bremen.de/cofi/CASL/lib/BD_Discussion.html

and please answer 

                      ***before end of May*** 

to the following questions:
  
  * Is the style of the Nat specification now optimal? - if not,
    please suggest improvements!

  * Are the symbols used in the Nat specification optimal? 
    (see the signature, which is separately available) - if not,
    please suggest improvements!

  * Are the axioms used to specify Nat optimal? - if not,
    please suggest improvements!

  * Do you agree with the style of the other libraries? - if not,
    please suggest improvements!

[Note that after the deadline, the authors are going to produce a new
 (hopefully nearly final) version of the basic datatypes.  NOW is the
 LAST CHANCE to influence the general style of these libraries... --PDM]

Greetings,
  Markus, Till, Lutz

-- 
----------------------------------------------------------
Markus Roggenbach                Phone +49-421-218-4683
Dept. of Computer Science        Fax +49-421-218-3054
University of Bremen             roba@tzi.de           
P.O.Box 330440, D-28334 Bremen   http://www.informatik.uni-bremen.de/~roba
----------------------------------------------------------