Re: CASL - Basic Datatypes

[Markus Roggenbach <roba@tzi.de>]

Dear Michel,

thank you for your reaction in time (!!!).

[Apologies for the delay with forwarding this and the following
 message.  In any case, despite the deadline that was set, I think
 the present discussion should continue until there is agreement on
 this important topic. --PDM]

Here our comments:

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

Good idea! As we currently develop the library just in an ASCII version,
we did not much work on display annotations, which of course have to be
included. 

> 2. What is the purpose of the unary +__ ?

Will be removed.

The operations 

	abs, rem, and quot

are introduced to have the signature of Nat as conform as possible with
the signature of Int. For integers the operations rem and quot are
different from div and mod.

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

The difference to our approach is, that we treat domain definitions as
`further properties' in case they are a consequences of the defining
axioms. I prefer here to expoit how the specification `works'.

> I have lost track of the rationale for distinguishing between the
> ExtSpec and the RichSpec. 

For `mathematical' structures like a partial order there are two
specifications: one for the `pure' concept [here: __<=__ with the
appropriate axioms] and an `enriched' one which also includes derived
operators, predicates, and sorts [here: inf, sup, __<__, __>__, __>=__].
One reason for this is that in general only the model class of the
`pure' version has the intended morphisms. As the derived operations,
predicates and sorts can be defined on top of any structure, which is a
model of the `pure' specification, it is quite natural to take the
`pure' version as a parameter of the `enriched' version. These are the
ExtSpecs. The RichSpecs are provided for those users who don't need/like
parametrization.

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

> * Is your use of SN = %def SPEC and SPEC2 legal ? What is the
>   rationale behind ?

Yes, it is legal  -- it applies to {SPEC and SPEC2} (c.f. the proposal
of %def in L-11). It becomes useful if there is a parameter and / or an
import. Thus I deliberately change your example to

	SN [Spec1] = %def Spec2 and Spec3

Now the annotation states that the extension Spec1 then {Spec2 and
Spec3} is definitional. Thus the rational is the same as for semantic
annotations in general: they are used to express known (or presumed)
features of the semantics of the specification.

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

I agree with your rationale, but maybe it should be refined:
ExtPartialOrder has PartialOrder as a parameter, which includes the sort
Elem. Thus Elem is already part of the parameter and it is exactly this
sort Elem, which is used in the instantiation. To have a second
parameter like in
 
   ExtPartialOrder [sort Elem][PartialOrder] = ...

could tempt the user to write

   ExtPartialOrder [sort X fit sort Elem |-> X]                 
                   [PartialOrder fit sort Elem |-> Elem, pred __<=__ |->
__<=__]

which is illegal.

Once again: thank you for your comments!

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