Re: CASL - Basic Datatypes

[Markus Roggenbach <roba@tzi.de>]

Michel,

after reading this mail I think you will agree that meanwhile our main
difference is where to place the definition domain axiom for partial
operations. I discuss this once again below - and as you write "But of
course this is matter of taste" I hope that you can accept our design
decision. 

The resulting specification of Nat is available at

        http://www.informatik.uni-bremen.de/cofi/CASL/lib/Nat_071.casl

1) Your arguments concerning abs, rem and qout in Nat are convincing:
We will remove these operations.

2) Concerning the general organization of our specifications we follow
the rules

        a) Arrange a basic specification in the order 

        Sorts ...
        Preds ...
        Ops ...
        Forall ...

        b) Add axioms that follow in an %implies part.
 
Rule a) allows to see the signature in a glance. According to Peter's
remark "I trust the authors to get the axioms right!" one might see
the signature as the most important information for the "external
user", even in the case of partial operations: of course we specify
the "expected" domain of partial operations. Since in most cases the
definition domain is a consequence of the defining axioms, the domain
axioms are currently in the %implies part, according to rule b).

Following your proposal to write the specifications in the order

a) The arity of the operation 
b) Its domain of definition if it is partial
c) The axioms that define it 
d) when appropriate, further properties, possibly in an implies part.

would mix up signature declarations with axioms and thus make it
difficult to see the signature in a glance.

I thought on your proposal and tried to collect the implied axioms not
in one extension (as we do it now) but instead to write them at the
first place where they can be formulated as implied axioms: this
strategy arranges the axioms for one operation in a more local
way. You can find the result for the specification NAT at

http://www.informatik.uni-bremen.de/cofi/CASL/lib/Nat_071_alternative.casl

- I don't think that this is a good solution.

Thus, I don't see a convincing alternative to our current way to arrange
the specifications.

3) Last point: 

> >> > Let consider ExtPartialOrder [PartialOrder]:
> >>
> >> > * What is the aim of Sigorder ?
> >>
> >> As the predicates __<__, __>__, __>=__ are part of many specifications,
> >> SigOrder summerizes their definitions in terms of __<=__ . This allows
> >> to add these predicates in a uniform way.
> 
> OK. From my experience with Larch (more precisely, my experience making
> engineers using Larch), this is more elegant but less clear. "naive users"
> may prefer to see explicitly these operations redefined if this results in a
> spec whose structure is much simpler and easier to grasp.

There are at most 3 imports of this type in the Basic Datatypes,and we
will remove them.


Greetings
  Markus

-- 
----------------------------------------------------------
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
----------------------------------------------------------