Wiki Agenda Contact English version

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;