Exact subtraction: Sterbenz's theorem
This function computes the exact subtraction if the inputs are near enough one to another.
Auteurs: Sylvie Boldo
Catégories: Floating-Point Computations
Outils: Frama-C / Jessie / Why3 / Coq
Références: 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;
}