Working with floating point numbers
Contents
Floating point numbers
One of the limitations with computers is the way that we have to represent real numbers. In a theoretical sense the real numbers has infinite range and infinite precision, however when we want to represent these numbers in a machine using the standard numerical representation for a variety of reasons we lose these properties.
Matlab and most computers use the IEEE 754 floating point standard. The standard defines the way real numbers can be represented from the bit level including the results of operations, and exceptions.
A full discussion of the standard is beyond the scope of this document we refer the interested reader to Matlab's documentation as well as the standard documentation
Proving tables with floating point numbers
The toolbox has support for proving tables with floating point inputs. Currently only PVS is supported for this feature, and in general manual intervention with the prover will likely be required.
Several new types are provided which can be used as anyother type in the input and output fields.
- single - a finite or infinite single precision number
- single_finite - a finite single precision number
- double - a finite or infinite double precision number
- double_finite - a finite double precision number
A sample input string might be "x:double_finite, y:double_finite". The same rules for subtyping still apply, as it may be necessary to subtype inputs in order to get them to typecheck properly.