The Why software verification platform can be used to translate code annotated with pre- and postconditions into proof obligations suitable for Gappa.

By installing Frama-C first and then Why (in order to build the Jessie plugin), one gets a tool for directly certifying C programs with Gappa.

The example below demonstrates the usage of these tools. The C
file defines a `sqrt`

function that computes the square root
with a relative accuracy of [math] for an input
`x`

between 0.5 and 2.

/*@ requires 0.5 <= x <= 2; ensures \abs(\result - 1/\sqrt(x)) <= 0x1p-6 * \abs(1/\sqrt(x)); */ double sqrt_init(double x); /*@ lemma quadratic_newton: \forall real x, t; x > 0 ==> \let err = (t - 1 / \sqrt(x)) / (1 / \sqrt(x)); (0.5 * t * (3 - t * t * x) - 1 / \sqrt(x)) / (1 / \sqrt(x)) == - (1.5 + 0.5 * err) * (err * err); */ /*@ requires 0.5 <= x <= 2; ensures \abs(\result - \sqrt(x)) <= 0x1p-43 * \abs(\sqrt(x)); */ double sqrt(double x) { int i; double t, u; t = sqrt_init(x); /*@ loop pragma UNROLL 4; @ loop invariant 0 <= i <= 3; */ for (i = 0; i <= 2; ++i) { u = 0.5 * t * (3 - t * t * x); //@ assert \abs(u - 0.5 * t * (3 - t * t * x)) <= 1; /*@ assert \let err = (t - 1 / \sqrt(x)) / (1 / \sqrt(x)); (0.5 * t * (3 - t * t * x) - 1 / \sqrt(x)) / (1 / \sqrt(x)) == - (1.5 + 0.5 * err) * (err * err); */ //@ assert \abs(u - 1 / \sqrt(x)) <= 0x1p-10 * \abs(1 / \sqrt(x)); t = u; } //@ assert x * (1 / \sqrt(x)) == \sqrt(x); return x * t; }

The code starts by calling the `sqrt_init`

function. It
returns an approximation of [math] with a
relative accuracy of [math]. Only the
specification of this auxiliary function is given. (Preconditions are
introduced by the `requires`

keyword, while postconditions are
introduced by `ensures`

.) Its implementation could use small
tables for instance. Note that bounds on relative errors are expressed as
[math] in this setting.

The `sqrt`

function then performs three Newton
iterations in order to obtain an improved approximation of the reciprocal
square root of `x`

. Since Gappa only handles
straight-line programs, a pragma annotation instructs Frama-C to
completely unroll the loop before passing it to Jessie. Finally, once the
reciprocal square root has been computed, it is multiplied by
`x`

to obtain the square root.

The `assert`

annotations cause Frama-C/Jessie to
generate additional proof obligations. These facts are then available to
the following proof obligations as hypotheses. In this example, the
actual content of the assertions does not matter from a certification
point of view, they are only used as a way to pass information to Gappa.
Indeed, as explained in the section called “Fixed-point Newton division”, Gappa needs to
know about Newton's relation and which expressions are approximations of
what. So, if the program were to be directly expressed in Gappa syntax,
the three loop assertions would instead have been written as
follows.

rsqrt = 1 / sqrt(x); err = (t - rsqrt) / rsqrt; { ... } u ~ 0.5 * t * (3 - t * t * x); (0.5 * t * (3 - t * t * x) - rsqrt) / rsqrt -> - (1.5 + 0.5 * err) * (err * err); u ~ rsqrt;

When writing these assertions for guiding Gappa, one just as to
make sure that they are easily provable; their actual accuracy is not
relevant. For instance, if the relative distance between
`u`

and [math] had been
[math] instead of [math],
Gappa would still have succeeded.

Passing the program above to the Frama-C/Jessie tool produces the following console output...

$ frama-c -jessie a.c [kernel] preprocessing with "gcc -C -E -I. -dD a.c" [jessie] Starting Jessie translation [kernel] No code for function sqrt_init, default assigns generated [jessie] Producing Jessie files in subdir a.jessie [jessie] File a.jessie/a.jc written. [jessie] File a.jessie/a.cloc written. [jessie] Calling Jessie tool in subdir a.jessie Generating Why function sqrt [jessie] Calling VCs generator. gwhy-bin [...] why/a.why Computation of VCs... Computation of VCs done. Reading GWhy configuration... Loading .gwhyrc config file GWhy configuration loaded... Creating GWhy Tree view...

...and displays the following user interface.

On the left of the window are the proof obligations. Once all of
them are proved, the code is guaranteed to match its specification. Green
marks flag proof obligations that were automatically proved. Selected
proof obligations are displayed on the right; here it is the
postcondition of the `sqrt`

function.

Gappa is not able to prove Newton's relation nor does it know that [math] holds. These assertions are therefore left unproved. Due to loop unrolling, Newton's relation appears three times. To factor these occurrences, a lemma describing the relation has been added to the C code. The Alt-Ergo prover is used to check that the three occurrences indeed match this lemma.

In the end, we have 72 proof obligations and only two of them are left unproved by the combination of Gappa and Alt-Ergo. They are mathematical identities on real-valued expressions, so they could easily be checked with an interactive proof assistant or a computer algebra system. (And they should be, at least for Newton's relation, because of its error-prone expression.)