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
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"
We suggest to abstract from the real numbers to a datatype REAL in a
two step manner:
The idea is that the step from
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.
- an intermediate step, reflected by the specifications
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
All three specifications of the final step are executable.
Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to email@example.com