## Wednesday, July 6, 2011

### Fast2Sum.v

Fast2Sum.v is a proof of the following procedure:
double Fast2Sum (double a, b) {double s = a + b;double r = b - (s - a);return r + s; }

See A floating-point technique for extending the available precision by T. J. Dekker.

So obvious, right?