A Formal Proof of Square Root and Division Elimination in Embedded Programs

Abstract : The use of real numbers in a program can introduce differences between the expected and the actual behavior of the program, due to the finite representation of these numbers. Therefore, one may want to define programs using real numbers such that this difference vanishes. This paper defines a program transformation for a certain class of programs that improves the accuracy of the computations on real number representations by removing the square root and division operations from the original program in order to enable exact computation with addition, multiplication and subtraction. This transformation is meant to be used on embedded systems, therefore the produced programs have to respect constraints relative to this kind of code. In order to ensure that the transformation is correct, i.e. preserves the semantics, we also aim at specifying and proving this transformation using the Pvs proof assistant.
Type de document :
Article dans une revue
Journal of Formalized Reasoning, ASDD-AlmaDL, 2013, 6 (1), pp.89-111
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00924367
Contributeur : Pierre Neron <>
Soumis le : lundi 6 janvier 2014 - 16:50:26
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 10 avril 2014 - 17:25:26

Fichier

JFRarticle.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00924367, version 1

Collections

Citation

Pierre Neron. A Formal Proof of Square Root and Division Elimination in Embedded Programs. Journal of Formalized Reasoning, ASDD-AlmaDL, 2013, 6 (1), pp.89-111. 〈hal-00924367〉

Partager

Métriques

Consultations de la notice

291

Téléchargements de fichiers

259