Pitfalls of a full floating-point proof: Example on the formal proof of the Veltkamp/Dekker algorithms

Abstract

Some floating-point algorithms have been used for decades and proved decades ago in radix-2, providing neither Underflow, nor Overflow occurs. This includes the Veltkamp algorithm, used to split a float into an upper part and a lower part and the Dekker algorithm, used to compute the exact error of a floating-point multiplication. The aim of this article is to show the difficulties of a strong justification of the validity of these algorithms for a generic radix and even when Underflow or Overflow occurs. These cases are usually dismissed even if they should not: the main argument In radix 2 of the first algorithm fails in other radices. Nevertheless all results still hold here under mild assumptions. The proof path is interesting as these cases are hardly looked into and new methods and results had to be developed. © Springer-Verlag Berlin Heidelberg 2006.