Computer Arithmetic and Formal Proofs

Verifying Floating-point Algorithms with the Coq System

Sylvie Boldo, Guillaume Melquiond

• Publisher: ISTE Press - Elsevier
• Year: 2017
• ISBN:
  9780081011706
• Topic: Computer Science
• Subtopic: Computer Science General
• Index: Computer Science

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs.

This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation.

• Describes the notions of specification and weakest precondition computation and their practical use
• Shows how to tackle algorithms that extend beyond the realm of simple floating-point arithmetic
• Includes real analysis and a case study about numerical analysis

1

Floating-Point Arithmetic

Abstract

Roughly speaking, floating-point (FP) arithmetic is the way numerical quantities are handled by the computer. Many different programs rely on FP computations such as control software, weather forecasts, and hybrid systems (embedded systems mixing continuous and discrete behaviors). FP arithmetic corresponds to scientific notation with a limited number of digits for the integer significand. On modern processors, it is specified by the IEEE-754 standard which defines formats, attributes and roundings, exceptional values, and exception handling. FP arithmetic lacks several basic properties of real arithmetic; for example, addition is not associative. FP arithmetic is therefore often considered as strange and unintuitive. This chapter presents some basic knowledge about FP arithmetic, including numbers and their encoding, and operations and rounding. Further readings about FP arithmetic include.

Keywords

AMD-K5 and AMD-K7; Computer arithmetic; Coq proof assistant; Flocq; FP algorithms; FP operations; IEEE-754 standard; Muller's sequence

Roughly speaking, floating-point (FP) arithmetic is the way numerical quantities are handled by the computer. Many different programs rely on FP computations such as control software, weather forecasts, and hybrid systems (embedded systems mixing continuous and discrete behaviors). FP arithmetic corresponds to scientific notation with a limited number of digits for the integer significand. On modern processors, it is specified by the IEEE-754 standard [IEE 08] which defines formats, attributes and roundings, exceptional values, and exception handling. FP arithmetic lacks several basic properties of real arithmetic; for example, addition is not associative. FP arithmetic is therefore often considered as strange and unintuitive. This chapter presents some basic knowledge about FP arithmetic, including numbers and their encoding, and operations and rounding. Further readings about FP arithmetic include [STE 74, GOL 91, MUL 10].

This chapter is organized as follows: section 1.1 provides a high-level view of FP numbers as a discrete set, and a high-level view of rounding and FP operations. Section 1.2 shows some simple results on the round-off error of a computation. Section 1.3 presents a low-level view of FP numbers, which includes exceptional values such as NaNs or infinities and how operations behave on them. Section 1.4 gives additional definitions and results useful in the rest of the book: faithful rounding, double rounding, and rounding to odd.

1.1 FP numbers as real numbers

We begin with a high-level view of FP numbers, which will be refined in section 1.3. A definition of FP formats and numbers is given in section 1.1.1. An important quantity is the unit in the last place (ulp) of an FP number defined in section 1.1.2. A definition of rounding and the standard rounding modes are given in section 1.1.3. Some FP operations and what they should compute are given in section 1.1.4.

1.1.1 FP formats

Let us consider an integer β called the radix. It is usually either 2 or 10. In a simplified model, an FP number is just a real value mβ^e satisfying some constraints on m and e given below. The integers m and e are called the integer significand and the exponent. The usual FP formats only consider FP numbers mβ^e with | m | < β^ϱ, with ϱ being called the precision. Let us also bound the exponent: e_min ≤ e ≤ e_max. An FP number is therefore a real value representable...

Table of contents

• Cover
• Title page
• Table of Contents
• Copyright
• Preface
• List of Algorithms
• Introduction
• 1: Floating-Point Arithmetic
• 2: The Coq System
• 3: Formalization of Formats and Basic Operators
• 4: Automated Methods
• 5: Error-Free Computations and Applications
• 6: Example Proofs of Advanced Operators
• 7: Compilation of FP Programs
• 8: Deductive Program Verification
• 9: Real and Numerical Analysis
• Bibliography
• Index