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