User's Guide for Gappa

Guillaume Melquiond


Table of Contents

1. Introduction
2. Invoking Gappa
Input and output
Command-line options
Embedded options
3. Formalizing a problem
Sections of a Gappa script
Preferred expressions and other peculiarities
Providing hints
4. Supported arithmetic
Rounding directions
Floating-point operators
Fixed-point operators
Miscellaneous operators
5. Examples
A simple example to start from: x * (1 - x)
Tang's exponential function
Fixed-point Newton division
6. Using Gappa from other tools
Why and Gappa
Coq and Gappa
7. Customizing Gappa
Defining a generator for a new formal system
Defining rounding operators for a new arithmetic
8. Bibliography
Description of Gappa
Applications of Gappa
A. Gappa language
Comments and embedded options
Tokens and operator priority
Grammar
Logical formulas
B. Warning and error messages
Syntax error messages
Other error messages during parsing
Proof failures
Warning messages during parsing
Warning messages during proof computation
C. Theorems of Gappa
Predicates
Theorems
D. Changes