Authors

Description

The libraries of CASL basic datatypes also illustrate how to write and structure specifications in CASL. All important features of CASL basic and structured specifications are used. The specifications in the libraries are carefully structured in such a way that interesting relations that should hold between the specifications can be expressed via semantic annotations. These annotations lead to proof obligations, which can be later discharged with a theorem proving tool, increasing the trust in the correctness of the specifications.

Beside the semantic annotations, we extensively use a set of annotations for operator precedences and an extension of the CASL syntax for literals. The underlying methodology of the here presented specifications is documented in the note M-6 ``Rules of Methodology''.

We also provide an index of all specification names. This index includes also all library names, which have the names of all their specifications as sub-entries.

An appendix provides some background material on the Basic Datatypes:

• the theory behind the datatypes ``exact fixed point numbers''
• graphical representations of the dependencies between the specifications
• the signatures (computed by the CASL tool set) of some selected specifications

The libraries of Basic Datatypes are still under construction.

The libraries of Basic Datatypes have been checked with CATS 0.41.

Specification