Sylvie Boldo

Gallery of proved programs

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