Download User's Guide for Gappa

Table of Contents
1. Introduction..................................................................................................................................... 1
2. Invoking Gappa............................................................................................................................... 2
2.1. Input and output ................................................................................................................... 2
2.2. Command-line options ......................................................................................................... 2
2.2.1. Selecting a proof back-end ...................................................................................... 2
2.2.1.1. Null back-end.............................................................................................. 2
2.2.1.2. Coq back-end .............................................................................................. 2
2.2.1.3. HOL Light back-end ................................................................................... 2
2.2.1.4. Coq back-end .............................................................................................. 3
2.2.2. Setting internal parameters ...................................................................................... 3
2.2.2.1. Internal precision ........................................................................................ 3
2.2.2.2. Dichotomy depth......................................................................................... 3
2.2.2.3. Fused multiply-add format.......................................................................... 3
2.2.3. Setting modes .......................................................................................................... 3
2.2.3.1. Assuming vague hypotheses ....................................................................... 3
2.2.3.2. Improving generated proofs ........................................................................ 4
2.2.3.3. Gathering statistics...................................................................................... 4
2.2.4. Enabling and disabling warning messages .............................................................. 4
2.3. Embedded options................................................................................................................ 5
3. Formalizing a problem ................................................................................................................... 6
3.1. Sections of a Gappa script.................................................................................................... 6
3.1.1. Logical formula ....................................................................................................... 6
3.1.1.1. Inequalities.................................................................................................. 6
3.1.1.2. Relative errors ............................................................................................. 7
3.1.2. Definitions ............................................................................................................... 7
3.1.3. Hints ........................................................................................................................ 8
3.2. Preferred expressions and other tricks ................................................................................. 8
3.2.1. Absolute and relative errors..................................................................................... 8
3.2.2. Global errors............................................................................................................ 8
3.2.3. Subsets of real numbers........................................................................................... 8
3.2.4. Disjunction .............................................................................................................. 9
3.3. Providing hints ..................................................................................................................... 9
3.3.1. Rewriting rules ........................................................................................................ 9
3.3.2. Approximated expressions .................................................................................... 10
3.3.3. Dichotomy search.................................................................................................. 10
4. Rounding operators ...................................................................................................................... 12
4.1. Rounding directions ........................................................................................................... 12
4.2. Floating-point operators ..................................................................................................... 12
4.3. Fixed-point operators ......................................................................................................... 13
4.4. Miscellaneous operators..................................................................................................... 13
4.4.1. Functions with relative error.................................................................................. 13
4.4.2. Rounding operators with homogen properties ...................................................... 14
5. Examples........................................................................................................................................ 15
5.1. A simple example to start from: x * (1 - x)........................................................................ 15
5.1.1. The C program....................................................................................................... 15
5.1.2. First Gappa version................................................................................................ 15
5.1.3. Defining notations ................................................................................................. 15
5.1.4. Complete version................................................................................................... 16
iii