# User’s Guide for Gappa

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques — automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs and circuits handling floating-point or fixed-point arithmetic.

This tool manipulates logical formulas stating the enclosures of expressions in some intervals. For example, a formal proof of the property

\[c \in [-0.3,-0.1] ~\land~ (2a \in [3,4] \Rightarrow b+c \in [1,2]) ~\land~ a-c \in [1.9,2.05] \quad \Rightarrow \quad b+1 \in [2,3.5]\]

can be generated thanks to the following Gappa script.

    { c in [-0.3,-0.1] /\
      (2 * a in [3,4] -> b + c in [1,2]) /\
      a - c in [1.9,2.05]

      -> b + 1 in [2,3.5] }

Through the use of rounding operators as part of the expressions, Gappa is specially designed to deal with formulas that could appear when certifying numerical codes. In particular, Gappa makes it simple to bound computational errors due to floating-point arithmetic.

Gappa is free software; you can redistribute it and/or modify it under the terms of the CeCILL Free Software License Agreement or under the terms of the GNU General Public License. (Refer to the files from the source archive for the precise wording of these two licenses.) Gappa can be downloaded on its project page. The tool and its documentation have been written by Guillaume Melquiond.

## Contents

- Invoking Gappa
  - Input and output
  - Command-line options
  - Embedded options
- Formalizing a problem
  - Sections of a Gappa script
  - Preferred expressions and other peculiarities
  - Providing hints
- Supported arithmetic
  - Rounding directions
  - Floating-point operators
  - Fixed-point operators
- Examples
  - A simple example to start from: x * (1 - x)
  - Tang’s exponential function
  - Fixed-point Newton division
  - Fast `nearbyint`
- Using Gappa from other tools
  - Why and Gappa
  - Coq and Gappa
- Bibliography
  - Description of Gappa
  - Applications of Gappa

## Appendices

- Gappa language
  - Comments and embedded options
  - Tokens and operator priority
  - Grammar
  - Logical formulas
- Warning and error messages
  - Syntax error messages
  - Other error messages during parsing
  - Proof failures
  - Warning messages during parsing
  - Warning messages during proof computation
- Theorems of Gappa
  - Predicates
  - Theorems

- Index