, Cette fois, il faut remplacer log 2 par Log2h + ? et distribuer un peu les opérations pour que Gappa se retrouve à devoir borner ((x ? k · Log2h) ? k · Log22) ? ((x ? k · Log2h) ? k · ?)
, Au nal, il aura su de fournir trois indications (les deux égalités et cette borne) pour que l'outil vérie automatiquement toutes les propriétés nécessaires de la réduction d'argument. Il ne reste alors plus qu'à utiliser Gappa pour combiner l'erreur de méthode, l'erreur d'arrondi de l'évaluation de la fonction rationnelle et l'erreur de la réduction d'argument et ainsi nir la vérication formelle de la fonction, Il sut alors d'indiquer à Gappa quelle est la diérence entre Log22 et ? = log 2 ? Log2h, diérence que intervaa n'a aucune diculté à borner
, Et dans un cas comme dans l'autre, la preuve s'appuie sur l'exécution d'un algorithme à base d'arithmétique d'intervalles à bornes ottantes. Ces algorithmes ont été vériés en Coq et sont exécutés au sein de Coq, Conclusion Nous avons vu comment prouver formellement et (presque) automatiquement des propriétés sur des expressions aussi bien à valeurs réelles qu'à valeurs ottantes
, la nalité est la preuve de théorèmes mathématiques, et dans l'autre, il s'agit de la vérication d'algorithmes numériques. De nombreuses pistes sont à explorer pour améliorer les bibliothèques et outils plus avant
, Pour ce qui est de Gappa, les résultats vériés automatiquement peuvent être puissants mais au prix d'indications parfois absconses de la part de l'utilisateur pour limiter la perte de corrélation. L'utilisation de formes anes symboliques pour représenter les erreurs d'arrondi ou d'un mécanisme équivalent permettrait peut
, C'est bien beau de vérier formellement une fonction C, mais qu'est-ce qui nous garantit que c'est eectivement elle qui sera exécutée au bout du compte ? Par exemple, un compilateur ne risquerait-il pas de faire l'optimisation décrite en section 4.3 ? C'est pour se prémunir de ce genre de problèmes que nous avons déni une sémantique précise pour le C et que nous avons prouvé formellement que le compilateur
,
, Veried compilation of oating-point computations, Journal of Automated Reasoning, vol.54, issue.2, p.135163, 2015.
, Coquelicot: A user-friendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, p.4162, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648
, Flocq: A unied library for proving oating-point algorithms in Coq, 20th IEEE Symposium on Computer Arithmetic (Arith), p.243252, 2011.
, Computer Arithmetic and Formal Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632617
, Using reection to build ecient and certied decision procedures, 3rd International Symposium on Theoretical Aspects of Computer Software (TACS), vol.1281, p.515529, 1997.
, Software Manual for the Elementary Functions, 1980.
, Certication of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, p.120, 2010.
, IEEE standard for oating-point arithmetic, IEEE Computer Society, 2008.
, Formally veried approximations of denite integrals, Journal of Automated Reasoning, 2018.
, Proving tight bounds on univariate expressions with elementary functions in Coq, Journal of Automated Reasoning, vol.57, issue.3, p.187217, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01086460
, Nathalie Revol, and Serge Torres. Handbook of FloatingPoint Arithmetic. Birkhäuser Basel, 2018.
, Roundo error cripples Patriot missile, SIAM News, vol.25, issue.4, p.11, 1992.
, Rigorous estimation of oating-point round-o errors with symbolic Taylor expansions, 20th International Symposium on Formal Methods (FM), vol.9109, p.532555, 2015.