Wiki Agenda Contact Version française

Exact subtraction: Sterbenz's theorem

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


Authors: Sylvie Boldo

Topics: Floating-Point Computations

Tools: Frama-C / Jessie / Why3 / Coq

References: NSV-3 Benchmarks

see also the index (by topic, by tool, by reference, by year)


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

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