When double rounding is odd

Sylvie Boldo 1 Guillaume Melquiond 1
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
Abstract : Double rounding consists in a first rounding in an intermediate extended precision and then a second rounding in the working precision. The natural question is then of the precision and correctness of the final result. Unfortunately, the used double rounding algorithms do not obtain a correct rounding of the initial value. We prove an efficient algorithm for the double rounding to give the correct rounding to the nearest value assuming the first rounding is to odd. As this rounding is unusual and this property is surprising, we formally proved this property using the Coq automatic proof checker.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00070603
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 8:59:07 PM
Last modification on : Thursday, January 17, 2019 - 3:16:03 PM
Long-term archiving on : Sunday, April 4, 2010 - 8:08:25 PM

Identifiers

  • HAL Id : inria-00070603, version 1

Collections

Citation

Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. [Research Report] RR-5400, 2004, pp.11. ⟨inria-00070603v1⟩

Share

Metrics

Record views

149

Files downloads

144