Floating point verification in HOL Light:
the exponential function
John Harrison ?
University of Cambridge Computer Laboratory
New Museums Site
Cambridge CB2 3QG
In that they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previously published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally.
Our main theorem connects the floating point exponential to its abstract
mathematical counterpart. The specification we prove is that the function has
the correct overflow behaviour and, in the absence of overflow, the error in
the result is less than :54 units in the last place (0:77 if the answer is denormalized)
compared against the exact mathematical exponential function. The algorithm is expressed in a simple formalized programming language, intended to be a subset of real programming and hardware description languages. It uses underlying floating point operations (addition, multiplication etc.) that are assumed to conform to the IEEE-754 standard for binary floating point arithmetic.
The development described here includes, apart from the proof itself, a formalization of IEEE arithmetic, a mathematical semantics for the programming language in which the algorithm is expressed, and the body of pure mathematics needed. All this is developed logically from first principles using the HOL Light prover, which guarantees strict adherence to simple rules of inference while allowing the user to perform proofs using higher-level derived rules. We first present the main ideas and conclusions, and then collect some technical details about the prover and the underlying mathematical theories in appendices.
?Supported by the EPSRC research grant `floating point verification'.