[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: CASL - Basic Datatypes
Dear CoFI Friends,
I react to Markus answer, but again I am not sure this is of interest to
anybody else, so please feel free to post it or not. [I do! --PDM]
On Thu, May 31, 2001 at 01:35:31PM +0200, Markus Roggenbach wrote:
>> Dear Michel,
>>
>> thank you for your reaction in time (!!!). 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.
Ok, fine.
>> > 2. What is the purpose of the unary +__ ?
>>
>> Will be removed.
Good.
>> 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.
I don't understand your purpose here. Either Nat will be used isolately,
and then the Int signature is irrelevant, and taking the absolute value of
a natural number is a bit akward; or one will use both Nat and Int
simultaneously, but then I expect Nat < Int and statements that ensure that
the result of some (Int-defined) f, when applied to Nat args, is of sort
Nat, i.e. I would rely on subsort overloading.
Hence you would have both abs: Int -> Nat and abs: Nat -> Nat, but at the
Int level, not before.
>> > 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'.
Again, I think that the purpose of the datatype library is to provide other
CASL users with easy to understand and use standard specs. For a "naive"
user, having to understand the subtleties of the design of the
specification may be asking too much.
>> > 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.
OK, thanks.
>> > 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.
>> > * 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.
For this specific use I am afraid the concrete syntax is quite misleading,
but I see your point.
>> > * 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.
OK.
Best regards,
Michel