This note consists of two intertwined parts:
The "Rules of Methodogy" give a guidline how to structure CASL specifications, provide a naming convention, suggest a labelling scheme for axioms, discuss how to deal with partial functions and subsorts within full CASL specifications, say how to devide specifications in parts, and propose techniques to keep overview.
The library covers datatypes like numbers, characters, strings and lists, together with specifications expressing their algebraic properties, like groups, rings and fields. Since the specification of real and complex numbers is quite involved, we have devoted a separate study note to them "The Datatypes REAL and COMPLEX in CASL" [MR99].
The standard library of CASL specification also illustrates how to write and structure specifications in CASL. All important features of CASL basic and structured specifications are used. The specifications in the library are carefully structured in such a way that interesting relations that should hold between the specifications can be expressed via semantic annotations.1
Throughout this note, we extensively use a set of annotations for operator precedences, a set of semantic annotations, and an extension of the CASL syntax for literals. The details of these annotations and syntax extensions are presented in our note "Proposal of Some Annotations and Literal Syntax in CASL" [RM99].
The note is organized as follows. Section 2 reflects the style of our proposal for basic datatypes in CASL. Section 3 contains the specifications itself, ordered by the subjects: concepts from order theory, concepts from algebra, boolean, numbers, finite sets, list and bag, pair, finite map and array, and characters and strings. Appendix A compiles some ideas how to realize numerical datatypes of programming languages in CASL, appendix B contains proofs about the specification of exact fixed point numbers.