Arithmétique des ordinateurs et preuves formelles

Résumé : Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste. Malheureusement, la machine utilise une arithmétique dite flottante, qui a ses contraintes. Ainsi, chaque calcul est effectué avec un certain nombre de chiffres (souvent environ 15 chiffres décimaux) et donc chaque calcul peut créer une erreur, certes faible, mais qui peut s'accumuler avec les précédentes pour fournir un résultat complètement faux. Ce cours montrera tout d'abord la façon dont l'ordinateur calcule, mais aussi comment compenser ou tirer partie de ces erreurs. Il présentera ensuite la notion de preuve formelle qui permet de s'assurer de la correction d'un théorème mathématique et de sa preuve. Avec cela, on pourra produire des preuves d'algorithmes qui utilisent l'arithmétique des ordinateurs.
Complete list of metadatas

Cited literature [40 references]  Display  Hide  Download

https://hal.inria.fr/hal-00755333
Contributor : Guillaume Melquiond <>
Submitted on : Wednesday, November 21, 2012 - 9:15:58 AM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Friday, February 22, 2013 - 3:47:11 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00755333, version 1

Collections

Citation

Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30. ⟨hal-00755333⟩

Share

Metrics

Record views

593

Files downloads

984