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