Prev Up Next
Go backward to 5 More About the Specification BasicReal
Go up to Top
Go forward to 7 A Specification of Complex Numbers

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:

The idea is that the step from BasicReal to AbstractExecutableReal is concerned with the discretization of the reals to a grid (screen), the points of which are the destination of a rounding. The step from AbstractExecutableReal to the three executable specifications of section 6.3 is a refinement of the AbstractExecutableReal to a finite floating point system.
  • 6.1 Screens and Roundings
  • 6.2 Proposal of an Abstract Datatype REAL
  • 6.3 Proposal of two Executable Datatypes REAL

  • CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
    Comments to

    Prev Up Next