De l’arithmétique d’intervalles à la certification de programmes

De l’arithmétique d’intervalles à la certification de
programmes

 La question de la valeur absolue

Considérons l’encadrement |e| ∈ [2, 5]. Il signifie que la valeur absolue de l’expression e est comprise entre 2 et 5. Mais si l’on regarde maintenant l’expression elle-même, cet encadrement signifie que la valeur de e est comprise dans les intervalles [−5, −2] ou [2, 5]. Autrement dit, e appartient à l’intervalle [−5, 5] mais n’appartient pas à ]−2, 2[. L’utilisation de la valeur absolue permet donc d’exclure des portions d’intervalles du domaine de certaines expressions. C’est utile pour appliquer un théorème dont le domaine de validité n’est pas connexe. Exemples de domaines non connexes C’est par exemple le cas pour l’erreur relative commise lors de l’arrondi d’un nombre réel en un nombre flottant. L’encadrement traditionnel E0 de cette erreur relative  = ◦(e)−e e n’est en effet valide que si la valeur de e n’appartient pas au domaine D0 des nombres dénormalisés. La contrainte pour appliquer le théorème pourrait donc être : avoir e ∈ I avec I ∩ D0 = ∅. Mais supposons que l’hypothèse dont on dispose soit en fait |e| ∈ [2, 5]. On peut en déduire une hypothèse e ∈ [−5, 5] mais la contrainte du théorème n’est alors pas respectée puisque D0 contient des valeurs proches de zéro. Le théorème reste cependant vrai si l’on modifie la contrainte en |e| ∈ I avec I ∩ |D0| = ∅. Si D0 est symétrique par rapport à zéro, cette nouvelle contrainte permet de prouver un plus grand nombre de propositions. Le seul risque est l’allongement de la preuve d’une étape s’il faut calculer un encadrement de |e| à partir d’un encadrement de e. Cette modification des contraintes ne se cantonne pas à l’erreur relative d’une opération flottante. Elle s’applique à toute réécriture impliquant un quotient. Ainsi,  pour pouvoir profiter de l’égalité e = 1/ 1 e , il faut disposer d’une hypothèse affirmant que e ne vaut pas zéro. Là encore, la contrainte est plus intéressante quand elle est exprimée à l’aide de la valeur absolue de l’expression : |e| ∈ I avec 0 6∈ I. Calculer avec des valeurs absolues Il est donc intéressant d’avoir des contraintes sur les encadrements de valeurs absolues. L’arithmétique d’intervalles n’est malheureusement pas efficace ici. Considérons par exemple que les hypothèses soient |x| ∈ [2, 5] et |y| ∈ [0, 1] et qu’il faille prouver x + y 6= 0. Cela signifie qu’il faut construire une hypothèse de la forme |x + y| ∈ I avec 0 6∈ I. Les seules propriétés intéressantes qui peuvent être ajoutées sont x ∈ [−5, 5] et y ∈ [−1, 1]. Par arithmétique d’intervalles, on peut alors en déduire |x + y| ∈ [0, 6]. Cette propriété n’est cependant pas suffisante. En faisant une trisection sur x entre les intervalles [−5, −1.5], [−1.5, 1.5] et [1.5, 5], on obtient une contradiction sur le domaine central et la propriété |x+y| ∈ [0.5, 6] sur les deux autres domaines. Ce qui prouve donc la validité de l’hypothèse |x+y| ∈ [0.5, 6], mais au prix d’une trisection. Afin d’éviter cette trisection et de réduire la taille de la preuve, il convient de mettre directement en relation l’encadrement de |x + y| avec ceux de |x| et |y| plutôt que de passer par ceux de x et y. Les inégalités triangulaire fournissent les inégalités |x| − |y| ≤ |x + y| ≤ |x| + |y|. Par simples addition et soustraction d’intervalles, on prouve que les expressions |x| − |y| et |x| + |y| prennent leurs valeurs dans les intervalles [1, 5] et [2, 6] respectivement. On en déduit alors |x + y| ∈ [1, 6]. Ce dernier encadrement satisfait la contrainte 0 6∈ [1, 6] et on a donc prouvé x + y 6= 0 sans avoir eu besoin de considérer des sous-domaines. 

Représentations améliorées

Jusqu’à présent, les expressions n’étaient encadrées qu’à l’aide d’un intervalle à bornes constantes. Afin de conserver plus d’informations de corrélation, on pourrait chercher à employer une représentation plus riche des encadrements. Les encadrements dépendraient d’expressions non constantes sur l’ensemble du domaine défini par les hypothèses. Même sans aller jusqu’aux séries formelles de Fluctuat [PGM04], voici deux représentations qui pourraient aider. Contrairement aux améliorations décrites précédemment, celles ci-après sont seulement à l’état de perspectives, elles n’ont pas été implantées dans Gappa. Représentation affine Les plus gros problèmes apparaissent quand on cherche à borner l’écart entre deux termes proches x˜ et x. Les encadrements de ces termes n’ont en effet plus aucune information concernant leur corrélation. Supposons maintenant que x˜ soit encadré en utilisant deux intervalles Xr et Xa : x˜ ∈ x · (1 + Xr) + Xa. Sous une  notation moins condensée, le prédicat est donc devenu : ∃ ∈ Xr ∃δ ∈ Xa x˜ = x · (1 + ) + δ. Un encadrement n’est donc plus un simple intervalle constant mais un triplet composé d’une expression et deux intervalles. Si les valeurs de l’expression x sont contenues dans l’intervalle X, il est alors facile d’en déduire un intervalle contenant la distance x˜ − x entre les deux termes : X · Xr + Xa. Quant à l’erreur relative, elle est contenue dans l’intervalle Xr + Xa/X. La composition d’erreurs ne pose pas plus de difficulté. Si les expressions x, y et z sont reliées par les encadrements y ∈ x·(1+Xr)+Xa et z ∈ y ·(1+Yr)+Ya alors z ∈ x · (1 + (Xr + Yr + Xr · Yr)) + (Xa + Ya + Xa · Yr). Dans la formule précédente, l’intervalle Xr+Yr+Xr·Yr devrait plutôt être évalué à l’aide de l’opérateur décrit au paragraphe 3.3.2. Des formules de complexité similaire permettent d’effectuer l’addition et la multiplication de deux encadrements x˜ ∈ x·(1 +Xr) +Xa et y˜ ∈ y ·(1 +Yr) +Ya. Par exemple, pour l’addition, on obtiendrait la formule suivante (l’autre opérateur décrit au paragraphe 3.3.2 serait ici indispensable pour limiter la décorrélation) : x˜ + ˜y ∈ (x + y) ·  1 + X · Xr + Y · Yr X + Y  + (Xa + Ya). L’avantage de cette représentation est que les réécritures présentées au paragraphe 3.2 deviennent inutiles pour des propagations directes de l’erreur : la représentation des encadrements fournit toutes les réponses. Qui plus est, il n’y a pas besoin de se préoccuper de prouver que des termes sont non nuls, contrairement à ce que l’on devrait faire si l’on manipulait directement des erreurs relatives. Dans le cadre des arithmétiques approchées à virgule flottante, les erreurs relatives d’arrondi sont perturbées par la présence non seulement de zéro mais aussi des nombres dénormalisés. Avec la représentation décrite ici, le problème ne se pose pas : il suffit de borner la petite erreur absolue commise dans le domaine des dénormalisés. Si l’on borne par 0 l’erreur relative en dehors des dénormalisés et par η0 sur le domaine des dénormalisés [Dem84], on obtient l’encadrement suivant : ◦(x) ∈ x · (1 + [−0, 0]) + [−η0, η0]. Si la dernière opération flottante effectuée est une addition ou une soustraction, cette représentation permet d’obtenir un résultat encore plus élégant : x⊕y est alors encadré par (x + y)·(1 + [−0, 0]). En effet, si x ⊕ y est un nombre dénormalisé, il vaut nécessairement x + y et l’erreur commise est alors nulle. Cette représentation améliorée présente cependant l’inconvénient de sa bien plus grande complexité. Non seulement les théorèmes ont à manipuler des prédicats plus complexes et leur vérification est plus longue, mais en fait ils n’existent parfois  même pas. On se retrouve alors contraint de revenir à des prédicats d’encadrement simple et d’appliquer les théorèmes classiques d’arithmétique d’intervalles. Une approche intermédiaire serait de ne pas utiliser systématiquement cette représentation améliorée. Ce serait juste un prédicat additionnel testé en parallèle du prédicat d’encadrement simple, au cas où il améliorerait les choses. Ce mécanisme de prédicat parallèle est déjà employé pour l’encadrement en valeur absolue présenté au paragraphe 5.2.3. Par conséquent, Gappa utiliserait généralement des encadrements simples associés à des réécritures. Mais en présence d’erreurs relatives et de nombres dénormalisés, l’outil pourrait se tourner vers les résultats fournis par ce prédicat amélioré. Modèles de Taylor L’utilisation de modèles de Taylor [MB03] s’apparente à la méthode décrite au paragraphe 3.3.1. Mais cette fois, au lieu de dériver formellement l’expression entière avant de l’évaluer, l’encadrement des diverses dérivées est construit au fur et à mesure de l’évaluation. Le prédicat d’encadrement est alors de la forme e ∈ P(x) + I avec I un intervalle et P un polynôme à coefficients représentables, c’est-à-dire des nombres dyadiques dans notre cas. L’arithmétique d’intervalles classique peut être considérée comme de l’arithmétique sur des modèles de Taylor dont le polynôme est nul. De la même façon que pour l’arithmétique d’intervalles, les opérateurs réels sont étendus aux modèles de Taylor. Ainsi, sachant que a ∈ P(x) + I et b ∈ Q(x) + J, l’encadrement de la somme a + b s’exprime a + b ∈ (P + Q)(x) + (I + J). Couplée aux réécritures d’expressions approchées, cette méthode permet même de gérer des expressions qui ne sont pas dérivables comme c’est le cas des fonctions contenant les opérateurs d’arrondi définis au chapitre 4. Considérons par exemple que l’on souhaite encadrer l’expression ◦(e). Il suffit d’encadrer l’erreur absolue ◦(e) − e par un intervalle J puis de réécrire l’expression ◦(e) en (◦(e) − e) + e. À supposer que l’expression e soit encadrée par P(x) + I, on obtiendra ◦(e) ∈ P(x) + (I + J). Comme pour la représentation affine, l’inconvénient est ici la plus grande complexité de cette représentation par rapport au simple intervalle et les difficultés que cela pose lors de la vérification des calculs. Qui plus est, il faut pouvoir décider quelle expression x sera choisie comme argument du polynôme. En effet, bien que l’on puisse construire des modèles de Taylor multivariés, il est préférable d’éviter la multiplication des indéterminées pour que les modèles puissent effectivement gérer les corrélations. 

Arithmétiques approchées en machine

Afin de prendre en compte les phénomènes d’arrondi, de nouveaux opérateurs sont ajoutés. Ce chapitre décrit leurs particularités et les liens qu’ils entretiennent avec l’arithmétique d’intervalles. Il présente aussi des prédicats spécialement adaptés aux ensembles de nombres dyadiques. Les chapitres précédents traitent d’une arithmétique idéale en précision infinie et montrent comment prouver des bornes d’expressions contenant les opérateurs arithmétiques de base sur R. L’un des objectifs de Gappa est néanmoins d’aider à certifier des applications numériques. Il est indispensable pour cela de savoir exprimer les opérations arithmétiques qu’elles contiennent. La précision et le domaine limités des formats manipulés en machine ont en effet tendance à perturber les résultats calculés par rapport aux valeurs obtenues en arithmétique réelle. En Gappa, ces nouvelles arithmétiques s’expriment à l’aide d’opérateurs d’arrondi. Des théorèmes exprimant les propriétés de ces opérateurs sont ensuite nécessaires pour que Gappa puisse les manipuler avec des intervalles. Cependant les intervalles ne sont pas tout à fait adaptés pour représenter des ensembles discrets de nombres machine, c’est pourquoi Gappa dispose aussi de prédicats permettant d’exprimer les propriétés de précision de ces nombres.

Opérateurs d’arrondi

Deux approches ont été successivement utilisées pour Gappa. La première, décrite au paragraphe 4.1.4, consiste à travailler directement sur les ensembles de nombres machine. La seconde, aujourd’hui utilisée dans l’outil, s’abstrait des problèmes de représentation en plongeant systématiquement les nombres machine 33 34 CHAPITRE 4. ARITHMÉTIQUES APPROCHÉES EN MACHINE dans l’ensemble des nombres réels afin de pouvoir appliquer aussi souvent que possible les théorèmes d’arithmétique réelle. C’est cette seconde approche qui est décrite ci-après. 4.1.1 Opérateurs unaires Même si les types numériques utilisés en matériel ne permettent pas de représenter tous les réels, un certain nombre de propriétés les rendent utilisables. Considérons deux nombres machine a et b. Si la somme réelle a + b de ces deux nombres est représentable par un nombre machine, alors l’addition en machine produira généralement ce résultat. Si le nombre n’est en revanche pas représentable, le résultat du calcul sera généralement un nombre qui en est proche. Ces propriétés permettent d’utiliser les arithmétiques machine comme substitut d’une véritable arithmétique des nombres réels. La norme IEEE-754 [IEE85] dicte ainsi que, en dehors des situations exceptionnelles, le résultat d’un calcul flottant s’obtient en calculant virtuellement la valeur réelle en précision infinie puis en l’arrondissant vers un nombre représentable en fonction du mode d’arrondi. C’est ce concept qui nous a conduit à introduire des opérateurs unaires d’arrondi. En effet, la somme approchée a ⊕ b va alors être égale à ◦(a+b), avec ◦ la fonction de R dans R qui se charge de calculer le nombre machine correspondant au résultat en précision infinie. Ainsi, au lieu d’avoir à définir tous les opérateurs arithmétiques approchés ⊕, , ⊗,, etc, il suffit de définir un unique opérateur d’arrondi ◦. Il en va de même pour les théorèmes. Les théorèmes d’arithmétique réelle n’ont besoin d’être prouvés qu’une seule fois. Il suffit ensuite de poser quelques théorèmes qui s’appliquent à un opérateur unaire et donc à toutes les opérations approchées de l’arithmétique correspondante. Un opérateur unaire différent est défini pour chaque arithmétique approchée. Le paragraphe 4.2 présente en détail quelques-uns des critères qui définissent un opérateur unaire : arithmétique à virgule fixe ou à virgule flottante, direction d’arrondi, précision du format de stockage, plus petite information représentable, etc. 

Opérateurs généralisés

Les opérateurs unaires peuvent ainsi être utilisés pour émuler un opérateur arithmétique approché à partir du moment où le résultat de l’opération dépend entièrement de la valeur du résultat de l’opérateur réel exact. Même si ce comportement est préférable du point de vue de la qualité des calculs, pour des raisons de performances ce n’est pas nécessairement le choix qui est fait dans certaines implantations [Tex97]. Considérons l’exemple d’un multiplieur en virgule fixe qui prend en entrée des nombres sur 32 bits avec une partie fractionnaire sur 16 bits. Le résultat est renvoyé dans ce même format et il y a plusieurs façons de l’obtenir. Pour respecter la règle selon laquelle ce résultat arrondi dépend entièrement du produit exact, il faudrait effectuer ce produit en totalité, ce qui nécessite un multiplieur entier 32×32 → 64 bits. Si seul un multiplieur 32 × 32 → 32 est disponible, une solution consiste à décaler chacune des entrées de 8 bits vers la droite, c’est-à-dire à diviser par 256 les entiers qui représentent les nombres à virgule fixe. Le produit de ces entiers représente une approximation du résultat réel dans le format initial. Appliquons cet algorithme aux produits (128 · 2 −16) ⊗ (512 · 2 −16) et (256 · 2 −16) ⊗ (256 · 2 −16). Le résultat en précision infinie vaut dans les deux cas 2 −16 . Mais la première multiplication répond 0 · 2 −16 tandis que la seconde répond 1 · 2 −16. L’utilisation d’un opérateur unaire n’est donc pas du tout adapté puisque ◦(2−16) peut prendre plusieurs valeurs. Il est par conséquent indispensable d’encoder dans l’opération d’arrondi la valeur des entrées. Au lieu de représenter le produit a ⊗ b par ◦(a × b), il faut donc plutôt le représenter par ◦×(a, b). Le principe de ces opérateurs généralisés peut être poussé un peu plus loin. Le résultat d’une opération peut en effet dépendre, non seulement des valeurs de chacune des entrées, mais aussi de leur représentation en machine, voire du contexte dans lequel l’opération a lieu. En conséquence, il peut être nécessaire d’ajouter un paramètre aux opérateurs afin de différencier des opérations qui bien qu’elles prennent les mêmes arguments en entrée produiraient des valeurs différentes en sortie. À chaque opérateur généralisé est associée une opération arithmétique réelle pour construire les énoncés des théorèmes le concernant. Ainsi, là où un théorème aurait fourni un moyen d’encadrer ◦(ab)−ab à partir d’un encadrement de ab pour un opérateur unaire, Gappa va chercher un théorème qui encadre ◦(a, b) − (ab) à partir d’un encadrement de ab pour un opérateur généralisé. À partir de là, il n’y a donc plus aucune différence entre opérateur unaire et opérateur généralisé. La syntaxe à base d’opérateurs unaires sera donc utilisée par la suite pour simplifier les notations. 

Limitations

Les opérateurs précédents sont conçus pour manipuler aussi souvent que possible des nombres réels plutôt que des nombres machine. Ils sont ainsi des fonctions de R n dans R. Seules les valeurs du format qui sont représentables dans R peuvent donc être manipulées et faire l’objet de théorèmes. Ainsi les formats flottants qui permettent de représenter des dépassements de capacité par des nombres se comportant comme −∞ et +∞ ne peuvent être traités que si ces nombres n’apparaissent jamais. Les théorèmes ne prennent jamais en compte ces situations exceptionnelles et se comportent comme si des nombres arbitrairement grands étaient représentables. Un programme conçu pour être résistant aux dépassements de capacité ne peut donc pas être directement traité par Gappa. Il faudrait considérer, à part, les cas exceptionnels à l’aide d’un autre formalisme. Cependant, la majorité des programmes ont été écrits en supposant que seuls des nombres finis sont manipulés lors de leur exécution. Une telle propriété du programme peut par contre être vérifiée à l’aide  de Gappa. Il suffit en effet de demander à l’outil de prouver qu’aucun des résultats ne se trouve en dehors du domaine des nombres représentables, ce qui est un simple encadrement d’expressions. Les infinis ne sont pas les seules valeurs qui échappent au formalisme utilisé par Gappa. Il n’est pas non plus possible de différencier des nombres différents représentant la même valeur réelle. C’est par exemple le cas des zéros signés en arithmétique flottante : pour Gappa, les nombres +0 et −0 de la norme IEEE754 sont le même réel zéro. Le signe du zéro n’a heureusement une importance que dans les situations exceptionnelles que Gappa ne gère de toutes façons pas. Finalement le formalisme ne permet pas non plus de gérer des nombres qui n’ont pas de signification dans R. C’est le cas des Not-a-Number, la racine carrée d’un nombre négatif par exemple.