Sections of a Gappa script

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;

Logical formula

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

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.

Relative errors

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.

Equalities

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.

Expression precision

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) }

Nonzero expressions

Finally, Gappa has special support for expressions that are not zero (and thus can be properly handled when they appear as denominators).

{ x <> 0 -> x / x in [1,1] }

Definitions

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

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.