[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Towards a new version of the CASL Basic Datatypes
[Sorry for the delay of the delivery of this message. BKB]
Markus, Till, and Lutz wrote:
> as agreed at the CoFI meeting in Berlin we have rewritten our
> specification of natural numbers, taking into account your various
> suggestions to improve it.
As this message may be a bit too long for most readers, let me try to
state my main points straight away:
* The proposed style of the libraries may well be ideal for the
purposes of those developing and maintaining them - HOWEVER:
* If that is THE way to specify Nat in CASL, critics may well accuse
CASL of having made (apparently) simple things look remarkably
complicated, which would be very bad PR for CoFI as a whole.
* Personally, I'd NEVER show the proposed Nat spec to a naive user,
since there'd be far too many things to explain all at once.
* One might produce a more user-friendly Nat spec by systematically
expanding all instantiations and views (and then suppressing the
definitions that are no longer referenced). If that is possible,
it'd be nice to see the result BEFORE approving the canonical
library spec of Nat.
* Some tools for producing "documentation views" of specs were
suggested at the Berlin meeting; they might allow the proposed
highly modular style proposed for the libraries to be adopted as
canonical, while supporting the automatic derivation of
user-friendly versions of the same specs for those who prefer them.
DETAILS
Thanks for the recent reminder of the deadline for comments (and
especially for its extension :-). As I wasn't at the Berlin meeting,
I'd been hoping to see comments first by some of those who were there.
Anyway, the following is based on my reading of the following bits
(which I cite almost in full, for ease of reference) from the Berlin
minutes:
Basic Datatypes
---------------
Markus Roggenbach presents the Study Note L-12 [...]
Michel Bidoit suggests to investigate Meta Theorems about CASL to
infer some (more complex) views automatically as this might simplify
the library - an issue for the Methodology Group, possibly a tool
issue as well. Then such consequences of specifications would be made
visible by a tool (or not!), similar to implicit axioms in datatype
definitions.
The issue how to incorporate (and map down to) sublanguages is
discussed at length. The present version includes alternative styles
as well, e.g. a partial pre as well as the total version due to
subsorting. There is agreement, that the presentation of the Basic
Datatypes to users ("documentation" version that could go along with
the Summary) should make full use of CASL (and should not be
artificially restricted to a particular sublanguage) as long as this
is natural; it should be as simple as possible. On the other hand,
some "user communities" present argue for a presentation of the Basic
Datatypes in a particular sublanguage since they need this for
particular tools: no subsorts, initially specified predicates,
conditional axioms (Genova), no partial functions but loosely
specified total functions (Saarbrücken), subsorts but no partial
functions (Nancy), initially specified operations for
consistency/implementability (Bremen, see Note M-8), property-oriented
"requirement", not "operational" specification at first glance
(Cachan), ... The problem of how to structure a specification to be
able to achieve projectability ("specification for re-usability")
without having to construct several co-existing specialised libraries
is general and real. Moreover, tool support to aid this would be very
valuable. Michael Kohlhase emphasises that tool support for
presentation of a particular view may resolve some of these issues.
Perhaps the "documentation" version should indeed be a particular
derived presentation rather than the original library.
[On the way back from Berlin, the Bremen group came up with some
possible solutions that have to be investigated further].
The authors of the Basic Datatype library will make proposals for a
more "user-friendly" presentation. On this basis, it receives
preliminary approval (and applause for the work that went into it).
> I. Some Remarks on our Rewritten Specification
> ==============================================
>
> In accordance with the suggestions made in Berlin,
>
> -> the only sorts are now Nat and Pos
> -> partial functions are not totalized by subsorting any more.
Is the latter simplification essential? Perhaps the provision of the
totalized functions might be useful for standardizing the interfaces
to CASL libraries from sub-languages?
> -----------------------------------------------
>
> II. The Signature of Nat
> ========================
>
> Sorts and subsorts:
>
> Nat >= Nat,Pos
> Pos >= Pos
It may be less confusing to present the above lines using CASL syntax.
> Operations:
>
> +__:Nat->Nat
> 0:Nat
> 1:Pos
> 1:Nat
> 2:Nat
> 3:Nat
> 4:Nat
> 5:Nat
> 6:Nat
> 7:Nat
> 8:Nat
> 9:Nat
> __! :Nat->Nat
> __*__ :Pos*Pos->Pos
> __*__ :Nat*Nat->Nat
> __+__ :Pos*Nat->Pos
> __+__ :Nat*Pos->Pos
> __+__ :Nat*Nat->Nat
> __-?__:Nat*Nat->?Nat
> __/?__:Nat*Nat->?Nat
> __@@__:Nat*Nat->Nat
> __^__ :Nat*Nat->Nat
> __div__ :Nat*Nat->?Nat
> __mod__ :Nat*Nat->?Nat
> __quot__:Nat*Nat->?Nat
> __rem__ :Nat*Nat->?Nat
> abs:Nat->Nat
> inf:Nat*Nat->?Nat
> max:Nat*Nat->Nat
> min:Nat*Nat->Nat
> pre:Nat->?Nat
> suc:Nat->Nat
> sup:Nat*Nat->?Nat
>
> Predicates:
>
> __<=__:pred(Nat*Nat)
> __<__ :pred(Nat*Nat)
> __>=__:pred(Nat*Nat)
> __>__ :pred(Nat*Nat)
> even:pred(Nat)
> odd :pred(Nat)
Again, one might use proper CASL syntax above for the predicate
declarations.
My impression is that for the majority of potential CASL users, the
above (together with a similarly-grouped list of all the specified
axioms) might be seen as the most user-friendly presentation of the
Nat spec...
> -----------------------------------------------
>
> III. The Specification Nat
> ==========================
>
> The whole specification text is available at
>
> http://www.informatik.uni-bremen.de/cofi/CASL/lib/BD_Discussion.html
>
> The following shows just the main specifications:
>
> %% PreNumbers
>
> spec SigPreNumbers [sort Elem] = [...]
> spec GenerateNat = [...]
> spec PreNat = [...]
> %% Numbers:
>
> spec SigNumbers[sort Elem][sort Exponent] = [...]
> spec Nat =
> ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Mult]
> with
> sorts Nat, Pos,
> preds __ <= __, __ >= __, __ < __, __ > __,
> ops 0, 1, suc, pre, __+__, __*__, __ ^ __
> and
> ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Add]
> with op __ ^ __ |-> __ * __
> and
> ExtTotalOrder [PreNat reveal sort Nat, pred __ <= __ ]
> with ops min, max
> and
> SigNumbers[sort Nat][sort Nat]
> then
In the present version of Note L-12, the specs for Relations and
Orders, PreNumbers, Algebra_I, and Numbers are found in separate
libraries. Hypertext presentations of the libraries would allow
users to go directly to referenced specs, but it might still be
preferable to show users everything involved in the Nat spec in a
single library (as the whole specification text referenced above
indeed does itself).
> -----------------------------------------------
>
> IV. About Parametrization
> =========================
>
> In the design of the Basic Datatypes, we have consistently implemented
> the following policy:
>
> Use parametrized specifications whenever they will be
> instantiated with different arguments.
>
> For the specification of datatypes like Lists, Stacks etc., this
> policy belongs to the folklore of the algebraic specification
> community. This policy usually also is applied if existing datatypes
> are extended with new functions, e.g. if the datatype of lists is
> extended with a sorting function.
>
> Now we also apply the policy in areas where it is less common to apply
> it. The most prominent area is algebra.
>
> For example, in the basic datatypes we have a specification
>
> spec Ring= ...
>
> which contains a sort Elem, constants 0 and e, binary operations * and
> +, and the usual axioms, and there is a `luxury version'
>
> spec ExtRing[Ring] = ...
>
> which introduces additional operations, in particular inverse
> operators and a power operator.
>
> It has been argued at the CoFI workshop in Berlin that applying the
> policy to algebra leads to too complex specifications.
I'm inclined to agree that the specs are much too complex for the
average user.
> Michel Bidoit has proposed the following workarounds: Write an
> unparametrized specification
>
> spec Ring2=
> Ring
> then ...
>
> containing the additional operators, and replace instantiations such
> as
>
> ExtRing[Int fit Elem |-> Int, e |-> 1]
>
> by
>
> Int then Ring2 with Elem |-> Int, e |-> 1.
>
> However, we think that this kind of workaround has important
> drawbacks, while the use of parameterized specifications have
> important advantages. These drawbacks resp. advantages are strong
> arguments in favour of use of parameterized specifications. We here
> repeat these (mostly well-known) arguments and show that they not only
> apply to the specification of Lists, sorting functions etc., but also
> to the specification of algebra.
>
> -- Compound identifiers:
> Using parametrized specifications guarantees correct renaming
> of compound identifiers. [...]
> -- Safety checks generated by instantiations: [...]
> -- Easy maintenance of specifications: [...]
> -- Further safety check through pushout property: [...]
> -- Easy re-use via views: [...]
>
> -- Good tool support: [...]
I agree that such use of parameterization and views has some
significant advantages - but it seems to me that they are mainly for
the benefit of those PROVIDING the libraries, and not so much for
those wanting to USE them. I'm afraid that I don't regard the
proposed spec of Nat as really "user-fiendly" at all.
> -----------------------------------------------
>
> V. Some Reasons to have the BDs in the CASL-Books
> =================================================
>
> There are two primary reasons to include the Basic Datatypes in the
> first place:
>
> a) They are the only existing example specification in CASL of
> appreciable size; moreover, they make use of all CASL features except
> architectural specifications. Thus, they are of particular didactic
> value.
Right - although that doesn't mean it's a good idea to use all CASL
features just in the spec of Nat...
> b) They are a prerequiste for the practical usability of CASL in the
> same way as the java beans are for java.
>
> Now both these aspects call for an actual reading of the specification
> text (where we regard `actual reading' as requiring the existence of
> the text *in print*): This is clear in the case of a). But also the
> actual use of the datatypes in other specifications requires the
> possibility of reading the text of the Basic Datatypes as an interface
> definition. (In fact, unlike in the case of libraries for programming
> languages, there is not much of a point in writing separate interface
> definitions for specification libraries, since these would not really
> look very different from the specifications themselves. [...].)
I don't agree with the last sentence above. While writing a library
that uses natural numbers, I'd reference the Nat spec, and bear the
exact signature in mind - but I probably wouldn't want to even look at
the axioms of Nat unless I was in doubt about the details of some
particular operation or predicate. (Similarly for a generic spec: I'd
want to see any axioms that the parameter spec might have, but
probably not those specified in the body.) I found the signature
listed under II above to be very helpful (read: essential) to get a
real overview of the Nat spec - if it hadn't been provided, I'd have
had to construct it for myself. I trust the authors to get the axioms
right!
A related point is that the development of further libraries may
suggest changes in the modular structure of the present libraries -
but such changes shouldn't affect the normal use of the present
libraries.
CONCLUSIONS ?
I wouldn't like to try to draw any conclusions before hearing other
opinions, especially as I may well have a badly-distorted perception
of the needs of "typical" CASL users.
However, if I might make some definite proposals for how to proceed,
they would be:
1. Ask the authors of L-12 to check that one can produce a
satisfactory "documentation view" spec of Nat systematically from
their present proposed spec, with:
- all auxiliary modules and views removed;
- all instantiations replaced by the resulting basic specs;
- (perhaps) declarations separated from axioms.
2. Provided that the result of 1 looks sufficiently user-friendly:
approve the proposed style for the revision of the libraries of
basic datatypes.
3. Ask the Tools group to coordinate the provision of tools (mentioned
in the Berlin minutes) for presentation of alternative views of the
same spec, with the production of the "documentation view" having
high priority.
4. Include only the "documentation view" of the main specs from the
libraries in the printed version of the envisaged CASL book - maybe
even in the User's Guide - making the original canonical library
specs accessible on CD-ROM and in hypertext documents on the web.
(The documentation view should remain rather stable, but the
structure and degree of parameterization of the canonical may
be changed without prior approval...)
Finally, I'd like to add my thanks to Markus, Till, and Lutz for all
their efforts with the basic libraries!
- -- Peter
========= ============================================================
==== ==== Peter D. Mosses mailto:pdmosses@brics.dk
========= BRICS & Dept. of Computer Science [= pdmosses@daimi.au.dk]
==== ==== University of Aarhus http://www.brics.dk/~pdm
==== ==== Ny Munkegade, bldg. 540 telephone: +45 8942 3285
==== ==== DK-8000 Aarhus C, DENMARK telefax: +45 8942 3255