06-these

Informations

• Publié par: Issi
• Nombre de lectures: 73
• Langue: Français

Extrait

◦ ◦N d’ordre:388 N attribuéparlabibliothèque:06ENSL0388
ÉCOLE NORMALE SUPÉRIEURE DE LYON
Laboratoiredel’InformatiqueduParallélisme
THÈSE
présentéeetsoutenuepubliquementle21novembre2006par
Guillaume MELQUIOND
pourl’obtentiondugradede
Docteurdel’ÉcoleNormaleSupérieuredeLyon
spécialité:Informatique
autitredel’Écoledoctoraledemathématiquesetd’informatiquefondamentaledeLyon
Del’arithmétiqued’intervalles
àlacertificationdeprogrammes
Directeurdethèse: Marc DAUMAS
Aprèsavisde: Guillaume HANROT
Christine PAULIN-MOHRING
Devantlacommissiond’examenforméede:
Jean Daniel B OISSONNAT Membre
Marc DAUMAS
Guillaume HANROT Membre/Rapporteur
John HARRISON Membre
Jean Michel M ULLER
Christine PAULIN-MOHRINGRemerciements
JetiensàremerciermondirecteurdethèseMarcDaumasd’avoirvulepotentiel
destravauxprésentésicietdem’avoirlaisséunegrandeliberté.
Je tiens à remercier Christine Paulin Mohring et Guillaume Hanrot d’avoir été
les rapporteurs de cette thèse, Jean Daniel Boissonnat d’avoir présidé, John Har-
risson d’être venu de si loin et Jean Michel Muller d’avoir complété le jury d’un
membrelocalmaisnéanmoinscompétent.
Je tiens à remercier mes coauteurs, Sylvie Boldo, Hervé Brönnimann, Florent
deDinechin,ChristophLauter,CésarMuñozetSylvainPion.
Je tiens à remercier Simone Criqui, Claude Pierre Jeannerod, Nathalie Revol
et Arnaud Tisserand pour leur relecture attentive de ce document. Toute faute que
vouspourriezydétecterprovientvraisemblablementdesretouchesdedernièremi
nutequej’aieffectuéesetnonpasd’unmanquedesérieuxdeleurpart.
Je tiens à remercier Francisco, Nicolas, Romain et Sylvain d’avoir été des co
1bureaux sympathiques . Je tiens à remercier les thésards du laboratoire qui ont su
me faire perdre de nombreuses heures dans des jeux en réseau : Damien, Florent,
Jérémie, Nicolas, Victor, Vincent. Les jeux en réseau ne sont pas la seule source
de non productivité et je tiens donc aussi à remercier Anne, Damien, Emmanuel,
Florent, Laurent, Stéphane et Stéphane, Sylvain et Sylvain. Comme tous les che
mins viennent de Lyon, il me faut aussi mentionner Benoît, Blaise, Christophe,
Emmanuelle et Emmanuel, Laurent, Philippe. Et enfin, Camille et Camille pour
leurréapparitionsurprise.J’aiprobablementoubliédenombreusespersonnesdans
ces quelques listes et, tôt ou tard, je me réveillerai en sursaut au milieu de la nuit
enmedisant:«Flûtine,j’aioubliéderemercierMachin!»
Je tiens à remercier les membres de l’équipe Arénaire qui ont su échapper aux
énumérations précédentes, en particulier Gilles Villard et Sylvie Boyer. Il faudrait
aussiquejeremercieleshabitantsdutroisièmeétage,Corinne,Dominique,Serge,
Simone, mais il y en a trop, je ne vais pas m’en sortir. Sans compter les ensei
gnants du département d’informatique de l’ENSL, ainsi que Jean François Pon
signon pour l’INSA. Et enfin, les étudiants qui m’ont subi pendant ces quelques
annéesdethèse.
CedocumenttientàremercierGedit,LatexetRubber.
Pourfinir:Pierre,onnet’oubliepas.
1Si votre prénom n’apparaît pas dans cette liste, ce n’est pas que vous m’êtes antipathique, c’est
justequevousavezdéjàétéremerciéunefois.Lamêmeremarques’appliqueauxlistessuivantes.
iiiTabledesmatières
1 Introduction 1
1.1 Certificationdecodesnumériques . . . . . . . . . . . . . . . . . 2
1.1.1 Bornesdevariablesetcomportementsinvalides . . . . . . 2
1.1.2 Erreursnumériques . . . . . . . . . . . . . . . . . . . . . 3
1.2 L’outilGappa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 Positionnement . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.3.1 Certificationformelledecodesarithmétiques . . . . . . . 6
1.3.2 Calculautomatiquedel’erreurd’arrondi . . . . . . . . . . 6
1.3.3 Certificationautomatiquedeprogrammes . . . . . . . . . 7
1.4 Plandudocument . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2 Preuveetarithmétiqued’intervalles 9
2.1 Preuves,ensemblesetinclusion . . . . . . . . . . . . . . . . . . . 10
2.1.1 Preuvedepropositions . . . . . . . . . . . . . . . . . . . 10
2.1.2 Réductionauxintervalles . . . . . . . . . . . . . . . . . . 11
2.2 Arithmétiqued’intervalles . . . . . . . . . . . . . . . . . . . . . 11
2.2.1 Typesalles . . . . . . . . . . . . . . . . . . . . . 11
2.2.2 Opérateursarithmétiques . . . . . . . . . . . . . . . . . . 12
2.2.3 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Lesintervallesenpratique . . . . . . . . . . . . . . . . . . . . . 14
2.3.1 Bornesd’intervalles . . . . . . . . . . . . . . . . . . . . 15
2.3.2 Croissanceetarrondidesbornes . . . . . . . . . . . . . . 16
2.3.3 Simplificationetoracle . . . . . . . . . . . . . . . . . . . 17
3 Intervallesetpertedecorrélation 19
3.1 Bissectiond’intervalles . . . . . . . . . . . . . . . . . . . . . . . 20
3.1.1 Exemplesetinconvénients . . . . . . . . . . . . . . . . . 20
3.1.2 Avantagesdelabissection . . . . . . . . . . . . . . . . . 21
3.2 Réécrituresd’expressionsd’erreur . . . . . . . . . . . . . . . . . 21
3.2.1 Àpartirdesarbressyntaxiques . . . . . . . . . . . . . . . 22
3.2.2 Àpartird’expressionsintermédiaires . . . . . . . . . . . 23
3.2.3 Autresréécritures . . . . . . . . . . . . . . . . . . . . . . 23
3.3 Améliorationd’encadrements . . . . . . . . . . . . . . . . . . . . 24
iiiiv TABLEDESMATIÈRES
3.3.1 Dérivationd’expressions . . . . . . . . . . . . . . . . . . 24
3.3.2 Nouveauxopérateursarithmétiques . . . . . . . . . . . . 25
3.3.3 Laquestiondelavaleurabsolue . . . . . . . . . . . . . . 28
3.3.4 Représentationsaméliorées . . . . . . . . . . . . . . . . . 29
4 Arithmétiquesapprochéesenmachine 33
4.1 Opérateursd’arrondi . . . . . . . . . . . . . . . . . . . . . . . . 33
4.1.1 Opérateursunaires . . . . . . . . . . . . . . . . . . . . . 34
4.1.2généralisés . . . . . . . . . . . . . . . . . . . 34
4.1.3 Limitations . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.1.4 Changerl’ensemblesous jacent . . . . . . . . . . . . . . 36
4.2 Représentations . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.1 Arithmétiqueàvirgulefixe . . . . . . . . . . . . . . . . . 37
4.2.2flottante . . . . . . . . . . . . . . . . . . . 38
4.2.3 Directionsd’arrondi . . . . . . . . . . . . . . . . . . . . 39
4.3 Théorèmesassociés . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.3.1 Bornesdevaleursarrondies . . . . . . . . . . . . . . . . 41
4.3.2 Erreursabsolues . . . . . . . . . . . . . . . . . . . . . . 42
4.3.3relatives . . . . . . . . . . . . . . . . . . . . . . 44
4.3.4 Réécritures . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.4 Prédicatsdeprécision . . . . . . . . . . . . . . . . . . . . . . . . 45
4.4.1 Prédicatdevirgulefixe . . . . . . . . . . . . . . . . . . . 46
4.4.2devirguleflottante . . . . . . . . . . . . . . . . 47
4.4.3 Exemple:Sterbenz . . . . . . . . . . . . . . . . . . . . . 47
5 FonctionnementdeGappa 49
5.1 Prétraitement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.1.1 Miseenformedespropositionslogiques . . . . . . . . . . 50
5.1.2 Recherchedescheminsdecalcul . . . . . . . . . . . . . . 51
5.2 Graphesdepreuve . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.2.1 Théorèmesetgraphesdepreuves . . . . . . . . . . . . . 53
5.2.2 Intersections . . . . . . . . . . . . . . . . . . . . . . . . 54
5.2.3 Encadrementsenvaleurabsolue . . . . . . . . . . . . . . 55
5.3 Bissections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
5.3.1 Déroulementd’unebissection . . . . . . . . . . . . . . . 56
5.3.2 Déclarationdebissections . . . . . . . . . . . . . . . . . 57
5.3.3 Découpageciblé . . . . . . . . . . . . . . . . . . . . . . 58
5.4 Règlesderéécriture . . . . . . . . . . . . . . . . . . . . . . . . . 60
5.4.1 Règlesprédéfinies . . . . . . . . . . . . . . . . . . . . . 61
5.4.2 Expressionsapprochéesetexpressionsexactes . . . . . . 61
5.4.3 Règlesutilisateur . . . . . . . . . . . . . . . . . . . . . . 62TABLEDESMATIÈRES v
6 Vérificationautomatique 65
6.1 Certificatsetapprocheoracle . . . . . . . . . . . . . . . . . . . . 66
6.2 Vérificationparlecalcul . . . . . . . . . . . . . . . . . . . . . . 67
6.2.1 Opérationssurlesnombresdyadiques . . . . . . . . . . . 68
6.2.2 Fonctionsbooléennes . . . . . . . . . . . . . . . . . . . . 70
6.3 Calculssimplifiés . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.3.1 Spécialisationdesthéorèmes . . . . . . . . . . . . . . . . 71
6.3.2 Gestiondesvaleursabsolues . . . . . . . . . . . . . . . . 73
6.3.3 Utilisationdesmultiplications . . . . . . . . . . . . . . . 73
6.3.4 Influencedelaprécision . . . . . . . . . . . . . . . . . . 74
6.4 Théorèmesetarrondis .