[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Towards a new version of the Basic Datatypes
Dear friends,
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.
We would like to ask you for feedback on our new specification until
January 19, 2001.
Based on your reactions we intend to rewrite the whole library of
Basic Datatypes. This new version shall be available early enough for
a thorough discussion at the CoFI meeting in Genua.
We hope to present in Genua a library of Basic Datatypes which - after
some minor changes - is in a shape that allows including it in the
CASL books.
Below you will find lots of material around our rewritten
specification, including
-> its signature and
-> its main parts.
The whole specification text is available at
http://www.informatik.uni-bremen.de/cofi/CASL/lib/BD_Discussion.html
[BKB: Note that the text does not include the new version of writing
annotations yet; in particular, the label annotations still precede
the axioms.]
Looking forward to your reactions!
Markus, Till, Lutz
-----------------------------------------------
Contents of the appendix:
I. Some Remarks on our Rewritten Specification
II. The Signature of Nat
III. The Specification Nat
IV. About Parametrization
V. Some Reasons to have the BDs in the CASL-Books
-----------------------------------------------
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.
BUT we decided to include some overloaded operators like
__*__ : Pos*Pos->Pos
__*__ : Nat*Nat->Nat
Without the operation __*__ : Pos*Pos->Pos, casts would be needed
e.g. within the definition of multiplication for the rational numbers:
generated type Rat ::= __ frac __ (Int;Pos)
vars i,j: Int; p,q:Pos
. %[Rat_equality] i frac p = j frac q <=> i*q = j* p
...
. %[Rat_mult_def] (i frac p) * (j frac q) = (i*j) frac (p*q)
Such additional casts are not only an inconvenience for the specifier,
but also lead to additional proof obligations concerning definedness
of terms.
Moreover, we decided not to change our policy on parametrized
specifications. Part IV of this appendix ("About Parametrization")
discusses this topic in detail.
-----------------------------------------------
II. The Signature of Nat
========================
Sorts and subsorts:
Nat >= Nat,Pos
Pos >= Pos
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)
-----------------------------------------------
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] =
SigOrder [sort Elem]
then ops 0: Elem;
__ + __, __ * __: Elem * Elem -> Elem %left assoc;
%prec { __ + __ } < { __ * __ }
end
spec GenerateNat =
free type Nat ::= 0 | suc(pre:? Nat)
end
spec PreNat =
GenerateNat and SigPreNumbers [sort Nat]
then
vars m,n: Nat
. %[Nat_leq_def1] 0 <= n
. %[Nat_leq_def2] not (suc(n) <= 0)
. %[Nat_leq_def3] suc(m) <= suc(n) <=> m <= n
. %[Nat_add__0] 0 + m = m
. %[Nat_add_suc] suc(n) + m = suc(n + m)
. %[Nat_mult_0] 0 * m = 0
. %[Nat_mult_suc] suc(n) * m = (n * m) + m
then %def
sort Pos = { p: Nat . p > 0 }
op %[PreNat_1_def] 1: Pos = suc(0) as Pos;
1 : Nat;
__*__: Pos * Pos -> Pos;
__+__: Pos * Nat -> Pos;
__+__: Nat * Pos -> Pos;
end
%% Numbers:
spec SigNumbers[sort Elem][sort Exponent] =
SigPreNumbers[sort Elem]
then SigPowerBinAlg[sort Exponent]
then %def
op +__: Elem -> Elem
%prec {+__} <> {__ ^ __}
var x: Elem
. %[plus_def] + x = x
then op abs: Elem -> Elem
end
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
preds odd, even: Nat
ops __! : Nat -> Nat;
__ -?__: Nat * Nat ->? Nat;
__ /? __: Nat * Nat ->? Nat;
__ div __, __ mod __ , __ quot __, __ rem __ :Nat * Nat ->? Nat;
%prec { __ -? __ , __ + __ } <
{ __*__, __ /? __, __div__, __mod__, __ quot __, __rem__ }
%prec { __*__, __ /? __, __div__, __mod__, __ quot __, __rem__ }
< { __ ^ __}
vars m,n,r,s: Nat; p: Pos
. %[Nat_abs] abs(n) = n
. %[Nat_odd_def] odd(m) <=> not even(m)
. %[Nat_even_zero] even(0)
. %[Nat_even_suc] even(suc(m)) <=> odd(m)
. %[Nat_factorial_zero] 0! = 1
. %[Nat_factorial_suc] suc(n)! =suc(n)*n!
. %[Nat_sub_def] m -? n = r <=> m = r + n
. %[Nat_divide_0] not def(m /? 0)
. %[Nat_divide_Pos] ( m /? n = r <=> m = r * n ) if n>0
. %[Nat_div]
m div n = r <=> (exists s: Nat . m = n*r + s /\ s < n)
. %[Nat_mod]
m mod n = s <=> (exists r: Nat . m = n*r + s /\ s < n)
. %[Nat_quot] m quot n = m div n
. %[Nat_rem] m rem n = m mod n
%% Operations to represent natural numbers with digits:
ops 1,2,3,4,5,6,7,8,9: Nat;
__ @@ __ : Nat * Nat -> Nat %left assoc
%number __@@__
vars m,n: Nat
. %[Nat_1_def] 1 = suc (0)
. %[Nat_2_def] 2 = suc (1)
. %[Nat_3_def] 3 = suc (2)
. %[Nat_4_def] 4 = suc (3)
. %[Nat_5_def] 5 = suc (4)
. %[Nat_6_def] 6 = suc (5)
. %[Nat_7_def] 7 = suc (6)
. %[Nat_8_def] 8 = suc (7)
. %[Nat_9_def] 9 = suc (8)
. %[Nat_decimal_def] m @@ n = (m * suc(9)) + n
then %implies
vars m,n,r,s,t: Nat; p: Pos
. %[Nat_sub_dom] def(m-?n) <=> m >= n
. %[Nat_divide_dom] def(m /? n) <=> m mod n = 0
. %[Nat_div_dom] def ( m div n ) <=> not (n=0)
. %[Nat_mod_dom] def ( m mod n ) <=> not (n=0)
. %[Nat_quot_dom] def ( m quot n ) <=> not (n=0)
. %[Nat_rem_dom] def ( m rem n ) <=> not (n=0)
. %[Nat_max_unit] max(m,0) = m
. %[Nat_distr] (r + s) * t = (r * t) + (s * t)
end
-----------------------------------------------
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. 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.
E.g., taking the actual specifications from the Basic Datatypes,
we see that in writing "Int then Ring with Elem |-> Int, e |-> 1"
as above, the user produces undesired effects: ExtRing (hence also
Ring2) contains compound identifiers, e.g. a sort RUnit[Elem] for
units of the ring, which would remain unchanged. Even supposing
that these become something like RUnit in Ring2, so that there is
no immediately visible `wrong name', this oversight will lead to
name clashes as soon as Ring2 is `instantiated' a second time.
-- Safety checks generated by instantiations:
In formal instantiations, it is checked that at least the signature
of the actual parameter really matches the formal parameter, and
proof obligations can be generated to deal with axioms;
alternative
methodologies provide no way at
all of catching such errors. E.g., the innocuous "Int then
Ring2" is wrong, since the `formal parameter' Ring contains a
unit e, to which the unit 1 in Int has to be explicitly matched;
not to mention things like "Nat then Ring2".
-- Easy maintenance of specifications:
Both the preceding points are crucial for the maintainability of
specifications: E.g., assume that the user of "Ring2" has noticed
his error and rewritten his specification as "Int then Ring2 with
Elem|->Int, RUnit|->RUnitInt, ...". If, at a later point of time,
Ring2 is modified to include a type Prime of prime elements, the
user is again saddled with an incorrect specification without even
knowing it. Worse things happen when "formal parameters" (i.e.,
the corresponding parts of the signature in the workaround) are
changed.
-- Further safety check through pushout property:
The much bemoaned (that includes ourselves) pushout conditions for
the well-formedness of instantiations do detect undesirable name
clashes and thus prevent the user from writing bad
(i.e. potentially inconsistent) specifications: If the same
symbols are defined in the body and in the actual argument
independently (which is illegal according to the pushout
semantics), they will usually be equipped with an intended and
often unique meaning expressed via appropriate axioms. Even if
these meanings happen to coincide at one stage of the development
process, they may diverge at a later stage, in particular since
the body and the actual argument will often be specified by
different persons.
-- Easy re-use via views:
Just as specifications, renamings can be reused; to this end, CASL
provides views, which can be used as argument fittings in proper
instantiations, but not in the workaround. Note that this is not
only another maintenance problem, but also a question of
usability, since lists of renamings may be substantially longer
than in our running example. Moreover, views carry proof
obligations which can be discharged once and for all, while
repeated explicit renamings will mean either repeated proving or
rather complicated searching for already proven statements.
-- Good tool support:
The development graph tool developed by the Inka people allows
to exploit the structure of specifications in various ways.
Many proof obligations can be discharged by just analysis
the graph structure of the development graph, e.g. by reducing
them to already proved ones. Moreover, there is a management of
change that allows to re-use developments and proofs when
the specification changes. All this works better if there is
more structure (e.g. in the form of parameterized specifications)
that can be exploited.
-----------------------------------------------
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.
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. It does, of
course, make sense to provide approximative descriptions in natural
language, a feature which is already present in Note L-12 as available
from the CoFI web site.)