Logo Hisseo

Approximation of the exponential function

The following program provides an approximation of the exponential function on interval [-1,1], using a Remez polynomial of degree 2.

Using Frama-C/Jessie with the strict-IEEE float model, we specify a bound on the total error expected from that function. An assertion in the code is inserted to express the mathematical error, that is without taking rounding in account.

#pragma JessieFloatModel(strict)

/*@ requires \abs(x) <= 1.0;
  @ ensures \abs(\result - \exp(x)) <= 0x1p-4; 
double my_exp(double x) {
  /*@ assert \abs(0.9890365552 + 1.130258690*x + 0.5540440796*x*x - \exp(x)) 
                  <= 0x0.FFFFp-4;
  return 0.9890365552 + 1.130258690*x + 0.5540440796*x*x;

This is proved by a combination of automated provers (SMT solvers and Gappa) and the Coq proof assistant.

The following screenshot shows that SMT solvers and Gappa verify all the verification conditions except the mathematical method error. The latter is verified inside Coq using the interval tactic, shown on the second screenshot below.

Coqide screenshot of proof of first verification condition: