6 Towards a Datatype REAL

Like in the appendix of our note M-6 [RM99a], we want to compile some ideas how to specify datatypes REAL of programming languages in CASL and how to relate them with the specification BasicReal. As computer arithmetic of floating point numbers is a rather subtle topic, some of our suggestions remain at an informal level. But we hope that they are detailed enough to be the basis for a discussion in the CASL community. The main references for the material presented in this section are the book "Computer Arithmetic in Theory and Practice" [KM81] and the article "What every computer scientist should know about floating-point arithmetic" [Gol91].

We suggest to abstract from the real numbers to a datatype REAL in a two step manner:

• an intermediate step, reflected by the specifications
  • ScreenAndRounding and
  • AbstractExecutableReal
  of section 6.2, which relies directly on the sort Real from the specification BasicReal. The theory behind this step is introduced in section 6.1, where we define the notions screen and rounding, and introduce different (normalized) floating point systems.
• a final step to a datatype REAL in a programming languages, which is discussed in section 6.3. Here we suggest on an informal level specifications
  • ExecutableRealKulischMiranker (based on [KM81]), and
  • ExecutableReal754 and
  • ExecutableReal854 (both based on IEEE norms).
  All three specifications of the final step are executable.