Back to Search Start Over

Floating-point arithmetic

Authors :
Sylvie Boldo
Claude-Pierre Jeannerod
Guillaume Melquiond
Jean-Michel Muller
Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA)
Inria Saclay - Ile de France
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF)
Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Arithmétiques des ordinateurs, méthodes formelles, génération de code (ARIC)
Laboratoire de l'Informatique du Parallélisme (LIP)
École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon
Institut National de Recherche en Informatique et en Automatique (Inria)
Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)
Centre National de la Recherche Scientifique (CNRS)
ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020)
European Project: 810367,EMC2(2019)
Source :
Acta Numerica, Acta Numerica, 2023, 32, pp.203-290. ⟨10.1017/S0962492922000101⟩
Publication Year :
2023
Publisher :
Cambridge University Press (CUP), 2023.

Abstract

Floating-point numbers have an intuitive meaning when it comes to physics-based numerical computations, and they have thus become the most common way of approximating real numbers in computers. The IEEE-754 Standard has played a large part in making floating-point arithmetic ubiquitous today, by specifying its semantics in a strict yet useful way as early as 1985. In particular, floating-point operations should be performed as if their results were first computed with an infinite precision and then rounded to the target format. A consequence is that floating-point arithmetic satisfies the ‘standard model’ that is often used for analysing the accuracy of floating-point algorithms. But that is only scraping the surface, and floating-point arithmetic offers much more.In this survey we recall the history of floating-point arithmetic as well as its specification mandated by the IEEE-754 Standard. We also recall what properties it entails and what every programmer should know when designing a floating-point algorithm. We provide various basic blocks that can be implemented with floating-point arithmetic. In particular, one can actually compute the rounding error caused by some floating-point operations, which paves the way to designing more accurate algorithms. More generally, properties of floating-point arithmetic make it possible to extend the accuracy of computations beyond working precision.

Details

ISSN :
14740508 and 09624929
Volume :
32
Database :
OpenAIRE
Journal :
Acta Numerica
Accession number :
edsair.doi.dedup.....8a81db438afc25763b2ff59c578340f8