Interval Semantics for Standard Floating-Point Arithmetic
For numerical computing practitioners and hardware designers, this work resolves long-standing ambiguities in the IEEE 754 standard by providing a consistent interval interpretation, enabling formal verification of floating-point algorithms.
The paper provides an interval semantics for standard floating-point arithmetic, interpreting non-zero finite numbers as point intervals and defining signed zeros and infinities to make previously undefined operations (0*inf, inf-inf, inf/inf, 0/0) well-defined, thus eliminating error conditions. This yields a mathematically sound basis for verifying numerical algorithms.
If the non-zero finite floating-point numbers are interpreted as point intervals, then the effect of rounding can be interpreted as computing one of the bounds of the result according to interval arithmetic. We give an interval interpretation for the signed zeros and infinities, so that the undefined operations 0*inf, inf - inf, inf/inf, and 0/0 become defined. In this way no operation remains that gives rise to an error condition. Mathematically questionable features of the floating-point standard become well-defined sets of reals. Interval semantics provides a basis for the verification of numerical algorithms. We derive the results of the newly defined operations and consider the implications for hardware implementation.