Real (and, to some degree, also complex) numbers should be a part of the CASL standard library, since they occur in many applications and programming languages. In this note, we address the specification of real and complex numbers at two levels: at the mathematical level and at the computer representation level.
At the mathematical level, we provide specifications of the mathematical concept of real (and complex) numbers. Only some part of these abstract real numbers can actually be represented on a computer. Nevertheless, the abstract concept is very useful as a mathematical ideal that can be approximated by computer representations. If we worked with approximating representations only, we would lose the nice mathematical properties of the abstract real numbers, and moreover, it would be much less clear what the underlying concept is that we approximate. We should mention that we do not present a theory that is strong enough to do real analysis. This would be possible, but we feel that at the level of the standard library, it suffices to have the real numbers plus the usual arithmetic and trigonometric functions - mainly those things occurring in programming languages. Still, our theory is strong enough to prove the (inner) uncountability of the reals.
At the computer representation level, we first provide a very loose specification of the concept of executable real numbers. A set of executable real numbers is a subset of the real numbers together with a rounding function (whereby both have to satisfy certain properties). We then sketch (without giving detailed specifications) two possible refinements of this specifications. The first one is based on more theoretical work, and ensures that important properties are not lost during rounding. The second one is the well-known IEEE standard. Finally, we briefly compare these two possibilities.
This note is organized as follows: section 2 gives a short overview on the datatypes specified in [RM99a], section 3 compiles a list of annotations proposed in [RM99b]. Based on these specifications and annotations we define datatypes DefineBasicReal and BasicReal in section 4. The theoretical background of these specifications is discussed in section 5. Section 6 compiles some ideas how to relate the specification BasicReal with datatypes REAL on computers. Finally, in section 7 we give a specification of the complex numbers.