Sylvie Boldo

Gallery of proved programs

All those programs were proved using the Bore version of Frama-C and the 2.26 version of Why. The Coq proofs use both the PFF and the gappalib libraries for Coq results about floating-point arithmetic.

Exact subtraction: Sterbenz's theorem

This function computes the exact subtraction if the inputs are near enough one to another.

/*@ requires  y/2. <= x <= 2.*y;
  @ ensures   \result == x-y;
  @*/

float Sterbenz(float x, float y) {
  return x-y;
}