John Harrison.
Technical Report
428, University of Cambridge Computer
Laboratory.

## Abstract:

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 0.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.

## Short version without appendices: DVI or
PostScript

## Shorter version still, to appear in AMAST: DVI or
PostScript

## Bibtex entry:

@TECHREPORT{harrison-style,
author = "John Harrison",
title = "Floating point verification in {HOL} {L}ight:
the exponential function",
institution = "University of Cambridge Computer Laboratory",
address = "New Museums Site, Pembroke Street,
Cambridge, CB2 3QG, UK",
year = 1997,
type = "Technical Report",
number = 428,
note = "Available on the Web as
{\verb+http://www.cl.cam.ac.uk/~jrh13/papers/tang.html+}"}