Download User Manual

B
Basic Library
Markus Roggenbach, Till Mossakowski, and Lutz Schröder
The Casl Basic Library consist of specifications of often-needed datatypes
and view among them, freeing the specifier from re-inventing well-know things.
This can be compared to standard libraries in programming languages. While
this user manual often discusses several styles of specifying with Casl, the
basic datatypes consistently follow a certain style described in [Mos03, VI.12].
We here describe two of the libraries (cf. the overview in Fig. B.1): the
library of numbers and of structured datatypes. We also provide strippeddown versions of the libraries themselves, with some of the specification and
all axioms and annotations removed. This stripped-down version can serve for
getting a first overview over the signatures of the specified datatypes.
The full Casl Basic Library is printed in the Casl Reference Manual
[Mos03, VI]. The latest version is available at
http://www.tzi.de/cofi
The Hets tool described in Chap. 10 allows you to obtain a graphical
overview over the specifications in the libraries and also inspect their signatures. We recommend to do this in order to get a better overview, and also
for answering specific questions that arise when using the basic datatypes.
B.1 Library Basic/Numbers
This library provides monomorphic specifications of natural numbers, integers, rational numbers, and rational numbers.
In the specification Nat, the natural numbers are specified as a free type,
together with a bunch of predicates and operations over the sort Nat of natural
numbers.
Note that the names for the partial operations subtraction −? and
division /? include a question mark. This is to avoid overloading with the
total operations − on integers and / on rationals, which would lead to
Possibly also in the CD coming with this
user manual, if there is one?