Re: CASL - Basic Datatypes

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

Dear Markus,

On Tue, Jun 26, 2001 at 02:52:17PM +0200, Markus Roggenbach wrote:
>> 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. 

Let me discuss again this issue, especially since I am afraid my
wording in my previous email was not as accurate as it should have been.
I don't comment points 1 and 3 since we now agree on them.

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

I agree with this, and frequently use this organization myself.

>> 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 did not meant the above as strictly as you have implemented it in 
http://www.informatik.uni-bremen.de/cofi/CASL/lib/Nat_071_alternative.casl
Just as a general design rule, which in my mind is compatible with your
preferred organization. Let me use "-?"(partial subtraction) as an
example. What I meant was:
a) you introduce -? in the signature part
Then in the "main axioms" (Forall) part, you state:
b) . def(m-?n) <=> m  geq  n          %(Nat_sub_dom)%
c) . m -? n = r <=> m = r + n         %(Nat_sub_def)%
Then if relevant you may mention further properties in an implies part (d)

So my main point is that, from a basic datatype library user point of view,
the fact that %(Nat_sub_dom)% can be derived from %(Nat_sub_def)% is
irrelevant, or at least less relevant than to see, grouped together in the
specification text, both the definition domain and the defining axiom, in
this order.

I would leave to the implies part less important properties, such as (just
for the sake of the example):
  . m -? (n1 + n2) = (m -? n1) -? n2

In other words, from a methodological point of view, I prefer, when it is
not totally obvious, an explicit specification of the definition domain,
even when it can be inferred from the other axioms provided. From my
experience, the average reader is not able to redo the corresponding
reasoning just by browsing the specification text.

Since you quote Peter's remark "I trust the authors to get the axioms
right!", I would like to add mine "I don't care if the authors didn't
choose the minimal axiomatization as long as they chose the most
clear one".

Especially for the basic data type library, I think I would personally
prefer to avoid implies as much as possible, preferring to group together
all relevant axioms for a given operation, when possible. The implies
annotations would rather be used for specifications written by the user,
since then these would be used to derive proof obligations and check the
relevance of the user's spec, not yours !
 
So, for the Basic/Number specification, I would indeed totally avoid
%implies. %(Nat_distr)% could fit nicely immediately after the
axiomatization of *. For %(Nat_max_unit)% and %(Nat_min_0)% (why max_unit
and not max_0 ?), this is really a matter of taste, but it would not hurt
to have these again immediately after the axioms defining max and min.

I hope I have been more clear this time, sorry for the misunderstanding
that arose from my previous email.

Best regards,
Michel