A Gappa script contains three parts. The first one is used to give names to some expressions in order to simplify the writing of the next parts. The second one is the logical formula one wants to prove with the tool. The third one gives some hints to Gappa on how to prove it.

The following script shows these three parts for the example of the section called “A simple example to start from: x * (1 - x)”.

# some notations for making the script readable @rnd = float<ieee_32, ne>; x = rnd(xx); y rnd= x * (1 - x); z = x * (1 - x); # the logical formula that Gappa will try (and succeed) to prove { x in [0,1] -> y in [0,0.25] /\ y - z in [-3b-27,3b-27] } # three hints to help Gappa finding the proof z -> 0.25 - (x - 0.5) * (x - 0.5); y $ x; y - z $ x;

This is the fundamental part of the script, it contains the logical formula Gappa is expected to prove. This formula is written between brackets and can contain any implication, disjunction, conjunction, negation of properties of mathematical expressions. These properties can be enclosures, inequalities, relative errors, equalities, and expression precisions. Any identifier without definition is assumed to be universally quantified over the set of real numbers.

Enclosures are either bounded ranges or inequalities. In positive position, ranges can be left unspecified. Gappa will then suggest a range such that the logical formula is verified.

{ x - 2 in [-2,0] /\ (x + 1 in [0,2] -> y in [3,4]) -> not x <= 1 \/ x + y in ? }

Results: x + y in [3, 5]

Note that Gappa might be able to prove the formula without even having to fill some unspecified ranges. In that case, Gappa will not display anything about them.

{ x in [1,2] /\ x - 3 >= 0 -> x + 1 in ? } # notice the contradiction between the hypotheses

Results: remaining results are pointless, anything can be proved.

Inequalities that give an upper bound on an absolute value are treated
specially. They are assumed to be full enclosures with a lower bound equal
to zero. In other words, `|x| <= 1`

is syntactic sugar for
`|x| in [0,1]`

.

Gappa does not know much about inequalities, as they never appear as
hypotheses of its theorems. They can only be used to refine a previously
computed enclosure. For instance, Gappa cannot deduce a contradiction from
`x * x <= -1`

alone. It needs to know either an enclosure of
`x`

or a nonnegative enclosure of `x * x`

.

The relative error between an approximate value `x`

and a more
precise value `y`

is expressed by `(x - y) / y`

. For
instance, when one wants to prove a bound on it, one can write:

{ ... -> |(x - y) / y| <= 0x1p-53 }

However, this bound can only be obtained if `y`

is (proved to
be) nonzero. Similarly, if a hypothesis was a bound on a relative error, this
hypothesis would be usable by Gappa only if it can prove that its denominator
is nonzero.

Gappa provides another way of expressing relative errors which does not depend on the denominator being nonzero. It cannot be used as a subexpression; it can only be used as the left-hand side of an enclosure:

{ ... -> x -/ y in [-0x1p-53,0x1p-53] }

This enclosure on the relative error represents the following proposition: [math].

As with enclosures, the range can be left unspecified.

{ x -/ x in ? }

Results: x -/ x in [0, 0]

When the bounds on a relative error are symmetric, the enclosure can be
written as `|x -/ y| <= ...`

instead.

While equalities could be encoded with enclosures,

{ ... -> x - y in [0,0] -> ...

Gappa also understands the following notation:

{ ... -> x = y -> ... }

Note that equalities are implicitly directed from left to right.
For instance, when looking for a property on `a + x`

, Gappa
will consider `a + y`

(assuming that property ```
x =
y
```

holds), but not the other way around. This is similar to the
handling of rewriting rules.

Whenever possible, equalities should be expressed as definitions rather than inside the logical formulas, as it offers more opportunities for Gappa to apply its theorems.

In addition to equalities and inequalities, Gappa also supports
properties about the precision needed to represent expressions. These
are expressed by using the predicates `@FIX(x,k)`

and
`@FLT(x,k)`

where `x`

is an expression and
`k`

an integer. Both properties state that `x`

can be decomposed as a generic binary floating-point number:
[math]. For
`@FIX`

this decomposition satisfies [math], while for `@FLT`

it satisfies [math]. For instance, the following Gappa formula
holds:

x = float<ieee_32,ne>(x_); { @FIX(x,-149) /\ @FLT(x,24) }

Typing the whole expressions in the logical formula can soon become annoying and error-prone, especially if they contain rounding operators. To ease this work, the user can define in another section beforehand the expressions that will be used more than once. A special syntax also allows to avoid embedding rounding operators everywhere.

First, rounding operators can be given a shorter name by using the
`@name = definition<parameters>`

syntax. `name`

can
then be used wherever the whole definition would have been used.

Next, common sub-terms of a mathematical expression can be shared by
giving them a name with the `name = term`

syntax. This name can then
be used in later definitions or in the logical formula or in the hints. The
equality itself does not hold any semantic meaning. Gappa will only use the
name as a shorter expression when displaying the sub-term, and in the generated
proof instead of a randomly generated name.

Finally, when all the arithmetic operations on the right side of a
definition are followed by the same rounding operator, this operator can be
put once and for all on the left of the equal symbol. For example, with the
following script, Gappa will complain that `y`

and `z`

are two different names for the same expression.

@rnd = float<ieee_32, ne>; y = rnd(x * rnd(1 - x)); z rnd= x * (1 - x); { y - z >= 0 }

Hints for Gappa's engine can be added in this last section, if the tool is not able to prove the logical formula. These hints are either rewriting rules or bisection directives. Approximate and accurate expressions can also be provided in this section in order to generate implicit rewriting rules.