Why and Gappa

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.

Example: floating-point square root

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.

Passing hints through annotations

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.

Execution results

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