[PDF] Spécification et vérification de systèmes paramétrés

View - Download Spécification et vérification de systèmes paramétrés

Previous PDF

Next PDF

Un Coq apprend à un bébé Colibri à flotter

Arthur Correnson

1and François Bobot2

1

ENS de Rennes, Rennes, Bretagne, France

arthur.correnson@ens-rennes.fr

2CEA, Gif-sur-Yvette, France

francois.bobot@cea.fr

Résumé

L"arithmétique flottante est connue pour être un sujet difficile. Ses propriétés contre- intuitives rendent l"écriture d"algorithmes manipulant les nombres flottants propice à de nombreuses erreurs. Des outils automatiques pour la vérification de programmes flottants existent mais ces outils faisant eux-mêmes usage de calculs en arithmétique flottante, on

peut se poser la question de leur propre fiabilité. Dans cet article, nous proposons de vérifier

formellement l"implémentation de raisonnements sur les nombres flottants dans le solveur de contraintes Colibri2. En particulier, nous présentons une méthodologie pour mener la preuve de correction de propagateurs de contraintes en utilisant l"assistant de preuve Coq.

Nous discutons également de l"intégration des raisonnements prouvés à un développement

logiciel complet en OCaml.

1 Introduction

1.1 Solveurs et résolution de contraintes

Les outils de raisonnement automatique sont de plus en plus utilisés dans le contexte de la

vérification formelle des logiciels. Parmi ces outils, les solveurs dits Satisfiabilité Modulo Théorie

(SMT) sont certainement les plus utilisés car ils permettent d"effectuer de manière automatisée

des preuves mobilisant plusieurs théories typiques des problèmes de vérification (théorie des

tableaux, théorie des flottants, ...). Le standard SMT-LIB [ 4 ] propose un language commun pour interroger les solveur SMT ainsi qu"un ensemble de théories usuelles dans lesquelles les solveurs SMT peuvent raisonner. Si le standard SMT-LIB définit un langage commun pour les

solveurs, il laisse en revanche complètement libre le choix des méthodes de résolution. Le solveur

Colibri2, nouveau successeur de COLIBRI, propose d"utiliser des méthodes de programmation

par contrainte (CP) pour la résolution de problème SMT. Un tel solveur interprète les problèmes

SMT comme des ensembles de contraintes reliant plusieurs variables. On cherche ensuite une affectation de chaque variable satisfaisant l"ensemble des contraintes. Les algorithmes utilisés

pour la résolution reposent sur l"idée de tenir compte de chacune des contraintes du problème

pour restreindre progressivement l"espace de recherche associé à chaque variable. On parle alors

de propagation de contraintes. Informellement, un propagateur de contrainte est une fonction

qui pour toute contrainte répond à la question suivante : " si la contrainte est satisfaite, que

puis-je en déduire sur la valeur de ses variables ». La correction d"un solveur CP est donc directement conditionnée par la correction des propagateurs de contraintes.

Après une présentation rapide de quelques difficultés notables liées à l"écriture correcte de

propagateurs flottants, nous proposons une méthodologie pour la preuve de tels propagateurs à l"aide de l"assistant de preuve Coq. Nous détaillerons également comment extraire le code Coq vers du code OCaml fiable et prêt à être intégré aux sources de Colibri2. Preuve formelle de propagateurs flottants A. Correnson, F. Bobot

1.2 L"arithmétique flottante et ses défauts

Représenter de manière exacte les nombres réels est impossible dans la mémoire finie d"un

ordinateur. Les nombres flottants répondent à ce problème et propose une approximation finie

des nombres réels permettant d"effectuer des calculs efficaces. De manière simplifiée, un nombre

flottant peut-être vu comme un réel que l"on peut écrire sous la formem2eavec(m;e)2Z. On contraint ensuite la taille demetepour assurer que tous les flottants ont une représentation finie. En imposant une précision (p) et des bornes sur l"exposant (eminetemax), on peut alors décrire un ensemble des nombres flottants comme F p;emin;emax=fm2ej jmj<2p^emineemaxg Notons qu"en fonction du choix des constantesp,eminetemaxil existe plusieurs ensembles de

flottants. D"une manière générale, une configuration(p;emin;emax)est appelée un format flot-

tant. Cette représentation est une vue très mathématique et ne convient pas à l"implémentation

de calculs effectifs sur les nombres flottants. Le standard IEEE-754 définit une représentation

binaire des nombres flottants sur 16, 32 et 64 bits (cela revient à fixer un format) et formalise le comportement attendu des nombres flottants en machine. En particulier, ce standard définit

la notion d"opérateur d"arrondi : des opérateurs permettant le passage d"un réel arbitraire au

flottant le plus proche dans un format donné. Plusieurs opérateurs d"arrondi sont définis par

le standard, le plus commun étant l"arrondi "au plus proche" aussi appelé RNE (round to nea- rest, ties to even). Pour simplifier la présentation dans la suite, on notera toujourso:R!F l"opérateur d"arrondi au plus proche.

Le standard IEEE-754 définit précisément les différentes opérations arithmétiques sur les

flottants ainsi que leur spécification. Dans la suite on noteramfpour l"addition flottante dans un mode d"arrondi donné (ou simplementfsi le mode d"arrondi n"a pas d"importance) etf, f,=fpour les relations binaires. Nous noterons les opérations réelles en suivant les notations conventionnelles des mathématiques. Une propriété fondamentale du standard IEEE-754 est qu"il impose que les opérations arithmétiques correspondent exactement à l"arrondi de leur pendant réel. Par exemple pour deux flottantsxetyon axfy=o(x+y). L"introduction de la notion d"arrondi entraîne des comportements tout à fait singuliers de

l"arithmétique flottante qui la rendent fondamentalement plus difficile que l"arithmétique réelle.

En particulier, selon l"ordre dans lequel les opérations binaires sont faites, on accumule les

erreurs d"arrondis et on perd de ce fait l"associativité de l"addition et de la multiplication par

exemple.

En plus des propriétés déjà soulignées, l"arithmétique des nombres flottants présente une

autre difficulté de taille : la présence des valeurs spéciales et des zéros signés. Dans les nombres

flottants, on s"autorise à manipuler les infinis comme des valeurs usuelles ce qui permet en particulier de donner un sens à la division par zéro. On admettra donc que1=0 =1dans

les nombres flottants. L"introduction des infinis comme valeurs oblige à étendre l"arithmétique

usuelle et à donner un sens à des expressions telles que+1 f1. On introduit donc une

valeur spéciale notéeNaNpour désigner le résultat de toute opération résultant en une valeur

non déterminée. Enfin, la présence d"un bit de signe dans la représentation mémoire des nombres

flottants tels que décrits dans le standard IEEE-754 différencie un zéro positif noté0+et un

zéro négatif noté0. L"égalité sur les flottants confond les deux zéros, mais1=0+=f+1alors

que1=0=f1. Ces singularités engendrées par l"introduction des valeurs spéciales doivent

être l"objet d"une attention toute particulière lorsque l"on écrit des algorithmes sur les nombres

flottants. 2 Preuve formelle de propagateurs flottants A. Correnson, F. Bobot

1.3 Raisonnements corrects sur les programmes flottants

Nous venons d"énumérer quelques-unes des nombreuses difficultés de l"arithmétique flot-

tante. Ces dernières rendent l"écriture d"algorithmes flottants particulièrement propices à des

erreurs de programmation pouvant avoir des conséquences désastreuses (l"accumulation d"er- reurs d"arrondis dans un calcul numérique de trajectoire de missile par exemple). Des outils de vérification formelle existent et permettent de valider la correction de programmes manipulant les nombres flottants [ 6 10 7 ]. Cependant, ces outils faisant eux mêmes l"usage de l"arithmétique flottante, on peut alors se demander ce qu"il en est de leur propre correction. Si ces derniers

produisent des résultats incorrects, la sûreté des programmes vérifiés par leur intermédiaire

peut-être compromise. L"effet est d"autant plus pervers que la confiance que nous donnons aux outils de vérification est grande.

Des initiatives pour prouver la correction des outils de vérification eux-mêmes ont déjà été

initiées [ 11 12 ]. Suivant cette idée, le solveur Colibri2 (développé en langage OCaml [ 2 ]) propose d"intégrer au sein même de son processus de développement la preuve formelle des composants les plus sensibles. Nous proposons dans cet article d"ajouter au solveur Colibri2 un support pour la théorie des nombres flottants. Cette extension consiste essentiellement en l"ajout de nouveaux propagateurs de contraintes spécifiques aux nombres flottants. Nous utiliserons l"assistant de preuve Coq [ 1 ] pour programmer et prouver ces propagateurs avant de les extraire pour les intégrer au solveur.

2 Résolution de contraintes, domaines et propagateurs

L"objectif final des travaux présentés dans cet article est l"intégration de raisonnements sur

les flottants prouvés corrects dans un solveur CP. Si on se concentre uniquement sur des pro-

blèmes simples de contraintes numériques (arithmétique entière, réelle ou flottante par exemple),

les solveurs CP raisonnent sur un ensemble de contraintes liantnvariablesx1;:::;xnau moyens des relations binaires et opérateurs arithmétiques usuels (=,,<,+,). En fonction de l"arith- métique considérée, les variables prennent leurs valeurs dans un ensembleE2 fZ;R;F32;:::get les contraintes peuvent être vues comme des fonctionsc:En!bool. Dans ce contexte, décider de la satisfiabilité d"une formule'revient à chercher une affectation2Endes variables telle que pour toute contraintecdans',c() =true. L"ensemble de toutes les affectations possibles E nest appelé l"espace de recherche et son sous-ensembleS'=f2Enj 8c2';c() =trueg est appelé espace des solutions. SiS'=;, il n"existe aucune solution et on dit que'est insa- tisfiable, dans le cas inverse'est satisfiable et toute affectation deS'est appelée modèle de Pour résoudre un ensemble de contraintes numériques', les solveurs analysent et combinent les contraintes pour collecter des informations sur les valeurs que peuvent prendre chaque va- riable et ainsi calculer une sur-approximationS'S'de l"espace des solutions. Pour chaque contraintec, on élimine dansSles affectations qui invalide trivialement la contraintec. On dit que l"on propage la contraintec. Initialement, on prendS=En, puis on propage toutes les contraintes dans'jusqu"à stabilisation deS'. Si au cours du processus,S'devient;alors' est insatisfiable. Si le processus converge vers une approximationS'6=;, on essaye d"extraire deSun modèle en choisissant une valeur pour chaque variable dans l"ordre (d"abord pourx1 puis pourx2, etc.). À mesure que des choix de la formexi=vsont faits, on peut propager ces décisions comme des contraintes. Si une décision provoque une contradiction, on l"annule ainsi que toutes les propagations qu"elle a engendré pour en faire une nouvelle : on parle de

backtracking. On alterne les phases de décision, propagation,backtrackingjusqu"à avoir affecté

3 Preuve formelle de propagateurs flottants A. Correnson, F. Bobot

une valeur à toutes les variables ou bien avoir testé toutes les décisions possibles sans succès.

En pratique on représente

Scomme une table qui associe à chaque expressioneapparaissant dans'des informations caractérisant une sur-approximation de son domaine d"appartenance. Ces informations peuvent être très simples (par exemple un intervalle d"appartenance) ou plus abstraites (par exemple une information de signe, un majorant, un bit connu, etc.) Intuitive-

ment, toute donnée décrivant un ensemble de valeurs peut être utilisée. Toutefois, on souhaite

a minimapouvoir propager ces informations à l"aide de propagateurs de contraintes. Les travaux de Marie Pelleau et ses collaborateurs [ 13 ] ont déjà mis en avant un lien fort entre cette notion de domaine dans le contexte des solveurs CP et la notion de domaine abstrait issue de la discipline de l"interprétation abstraite [ 9 ]. Ce rapprochement donne un cadre théorique utile pour exprimer le comportement attendu des propagateurs de contraintes et ainsi élaborer

leur preuve de correction. Nous rappelons à présent quelques définitions inspirées par ces travaux

et qui nous serviront par la suite de support pour la preuve de propagateurs flottants. Définition 2.1(Domaine abstrait sur un ensembleE).On appelle domaine abstrait sur l"en- sembleEla donnée d"un quadruplet(D;>;?; )où : -Dest un ensemble et :D! P(E)est une interprétation des éléments deDcomme des parties deE. -? 2Dreprésente l"ensemble vide ( (?) =;) et permet de caractériser les contradictions. -> 2DreprésenteE( (>) =E) et permet d"initialiser l"espace de recherche.

Dans le contexte de la résolution de contraintes, on équipe également les domaines abstraits

avec les opérateurs suivants : Un op érateurd"in tersectionu:DD!Dqui permet de combiner deux informations connues sur une expression. P ourc haqueop érateurarithmétique :EE!E, un opérateur abstrait]:DD! Dqui permet d"assigner un domaine aux expressions arithmétiques. P ourc haquerelation binaire EE, un propagateur de contrainte:DD! DD. Il permet de raffiner les informations connues sur deux expressionse1ete2sous l"hypothèse quee1e2. Pour garantir la correction des solveurs, on impose que ces nouveaux opérateurs aient cer- taines propriétés. Hypothèse 2.1(Correction deu).Soientd1etd2deux éléments deDetxun élément deE, on impose que (d1)\ (d2) (d1ud2). Hypothèse 2.2(Correction des opérateurs).Soit:EE!Eet soientd1etd2deux

éléments deD, on impose quefxyjx2

(d1)^y2 (d2)g (d1]d2). Hypothèse 2.3(Correction des propagateurs).Soit EEune relation binaire, soient d

1etd2deux éléments deD, soit(d01;d02) =(d1;d2)et soientxetydeux éléments deE, on

impose deux propriétés : -améliored1etd2: (d01) (d1)^ (d02) (d2) -respecte: Sixyalorsx2 (d01)^y2 (d02) Les propriétés de correction des propagateurs et des opérateurs abstraits assurent que leur utilisation permet toujours de calculer une sur-approximation de l"espace de recherche. Le fait que les propagateurs améliorent les domaines permet de garantir la convergence des solveurs : on ne fait jamais grossir l"espace de recherche en propageant une contrainte. 4 Preuve formelle de propagateurs flottants A. Correnson, F. Bobot

2.1 Domaine d"intervalles

Pour illustrer la démarche adoptée pour le développement et la preuve d"un domaine abstrait,

nous prenons l"exemple des intervalles flottants. En présence de contraintes d"inégalités, ce

domaine abstrait s"avère très utile car il permet d"identifier rapidement des bornes inférieures

et supérieures pour chaque variable du problème à résoudre. Par exemple pour le problème

':=fx3^x4g, l"utilisation d"un domaine d"intervalles révèle immédiatement que'est insatisfiable après deux propagations : 1. On note dxle domaine dexet on initialisedx:=>=f1;+1g 2. On propage la con traintex3:dxdevientfst((dx;f3;3g)) =f1;3g 3. On propage la con traintex4:dxdevientfst((dx;f4;4g)) =?

4.dx=?, sans possibilité debacktrackingla résolution prend fin et'est insatisfiable.

Dans les réels, il est d"usage de définir les intervalles comme des pairs(a;b)2R2. L"ensemble dénoté par l"intervalle(a;b)est ensuite défini commefx2Rjaxbg. Pour permettre un

meilleur découpage deRen intervalles, on prolonge généralement cette définition en autorisant

des bornes dansR:=R[ f1;+1get on distingue les bornes d"intervalles strictes et non

strictes. Dans les flottants, les infinis sont des valeurs usuelles et peuvent donc être traitées

indistinctement des autres. De plus, la finitude des nombres flottants permet de définir les

opérateurs unairepredetsuccqui à tout flottant associe respectivement son prédécesseur et

son successeur autorisant ainsi à ramener les tests d"inégalités strictes à des tests d"inégalités

larges. Les notions de bornes strictes et non strictes peuvent donc être ignorées dans le cas flottant. La présence duNaNperturbe la définition des intervalles flottants. Rappelons que la valeur NaNn"est pas comparable, c"est à dire que8x2F;:(xNaN_NaNx)(avec 2 ff;f f;>f;=fg). Tout intervalle flottant ayant une borneNaNreprésente donc un intervalle vide et par conséquent il n"existe pas d"intervalle contenantNaN. Néanmoins, dans le contexte d"un

solveur, modéliser la possibilité qu"une expression puisse prendre la valeurNaNest utile. En effet

prendre en compte la valeurNaNpeut permettre de détecter des contradictions supplémentaires

et donc d"accroître les capacités de résolution des solveurs. Par exemple, toute contrainte de la

formexNaNest insatisfiable et il est souhaitable qu"un domaine d"intervalle soit en mesure de

capturer cette propriété. Pour prendre en compteNaN, nous étendons la définition des intervalles

flottants commeI(F) =F2bool. Un triplet(a;b;nan)2F2booldénote l"ensemblefx2

Fjafxfb_(x=NaN^nan)g.

Nous définissons à présent les opérateursu,+]etassociés au domaine abstrait des intervalles et tels que spécifiés précédemment.

Définition 2.2(Concrétisation).Les éléments deI(F)peuvent être interprétés comme des

parties deFpar la fonction de concrétisation définie comme : ((a;b;nan)):=fx2Fjaxb_(x=NaN^nan)g Définition 2.3(Intersection).L"intersection peut se définir de la façon suivante : (a;b;nan)u(a0;b0;nan"):= (max(a;a0);min(b;b0);nan^nan") Théorème 2.1(Correction et précision de l"intersection).Soientd1;d2deux intervalles de

I(F), alors :

correction : 8x2F;x2 (d1)^x2 (d2))x2 (d1ud2) précision : 8x2 (d1ud2);x2 (d1)^x2 (d2) 5 Preuve formelle de propagateurs flottants A. Correnson, F. Bobot

Démonstration.Par analyse de cas sur les valeurs nan et nan", et à l"aide des propriétés dumax

et duminon obtient la précision et la correction deu.Définition 2.4(Opérateurs abstraits).Les opérateurs abstraits]s"obtiennent à partir des

opérateurs binaires. Nous prenons l"exemple de l"addition : (a;b;n) +](a0;b0;n0):= (afa0;bfb0;n_n0__ x2fa;a0g y2fb;b0gsum-to-nan(x;y)) avec sum-to-nan(x;y)si et seulement sixfy=NaNc"est à dire sixetysont deux infinis opposés ou si l"une des deux valeurs estNaN. Théorème 2.2(Correction de l"addition abstraite).Soientd1;d2deux intervalles deI(F), alors

8(x;y)2F2;x2

(d1)^y2 (d2) =)xfy2 (d1+]d2) Démonstration.Soientd1= (a;b;nan)etd2= (a0;b0;nan"), on raisonne par analyse de cas selon que les bornesa,a0,b,b0et la sommexfysoientNaN,1, ou des valeurs finies. Dans les cas où les trois sommesafa0,xfyetbfb0sont différentes deNaN, la monotonie de l"addition flottante s"applique (voir 3.2 ) et on peut déduire des hypothèses queafa0fxfyfbfb0 et donc quexfy2 (d1+]d2). Dans les autres cas, les règles de l"arithmétique flottante pour

les valeurs spéciales s"appliquent et la preuve s"achève par simple calcul.Les propagateurs de contraintespeuvent être définis en deux temps. Dans un premier

temps nous définissons un opérateur:D!Dqui calcule le domaine des candidats à la satisfaction de la relationpar rapport à un domaine donné. Formellement on souhaite que (d) fy2Fj 9x2 (d);yxg. Par exemple pour les comparaisons flottantesfetfon a : (a;b;nan):=ifb All.html. La méthodologie employée pour les preuves est présentée en détail dans la partie3 .

D"autres développements proposent également de prouver formellement des domaines flottants en utilisant l"assistant de preuve Coq. C"est le cas notamment du projet Verasco [ 11 ] qui propose une implémentation en Coq de plusieurs domaines abstraits dont des domaines flottants. Les

domaines flottants de Verasco sont développés dans le contexte de la vérification par interpré-

tation abstraite et ne traitent que des flottants de format32ou64bits. L"implémentation que nous proposons est générique pour tout format flottant.

2.2 Correction complète d"un solveur CP

La correction des propagateurs ne suffit pas à assurer la correction complète d"un solveur

CP. En effet, d"autres paramètres sont à considérer dont notamment la terminaison. De même,

il faut s"assurer que l"algorithme qui orchestre la résolution fait une utilisation raisonnable des

propagateurs. La démarche de prouver formellement l"algorithme de résolution de Colibri2 a

déjà été amorcée mais nous ne détaillerons pas ici ces aspects. Notons toutefois que la preuve

de correction et de terminaison d"un algorithme de résolution de contraintes requiert que les

propagateurs utilisés soient corrects et, à ce titre, notre démarche constitue déjà une étape

importante dans l"élaboration d"une telle preuve. Prouver formellement un algorithme de résolution de contraintes dans un assistant à la démonstration ou tout autre outil de vérification formelle (comme Why3 par exemple [ 5 ]) re-

présente un coût de développement conséquent. De ce fait, les fragments entièrement prouvés

de Colibri2 sont modestes et fournissent un moteur de résolution correct mais peu puissant. En

prouvant les propagateurs séparément, les mêmes propagateurs prouvés peuvent-être utilisés

aussi bien dans un algorithme de résolution entièrement formalisé (auquel cas, les preuves de

correction des propagateurs jouent un rôle dans la preuve de correction du solveur entier), que

dans un algorithme de résolution plus avancé pour lequel on tolère l"absence d"une preuve de

correction complète (dans ce cas, la simple correction des propagateurs donne déjà des garanties

fortes).

3 Formalisation Coq des nombres flottants

3.1 La bibliothèque Flocq

Nous souhaitons intégrer au solveur Colibri2 un support minimal pour la théorie des nombres

flottants. Nous proposons à cet effet une implémentation Coq du domaine d"intervalles flottants

présenté dans la partie 2.1 . Cette implémentation est ensuite traduite en code exécutable afin

d"être intégrée dans les sources du solveur. Pour atteindre ces objectifs, nous avons besoin

d"une modélisation des nombres flottants au sein de l"assistant de preuve Coq. Cette même

modélisation sera utilisée dans les preuves mais également comme implémentation de référence

de l"arithmétique flottante. Utiliser la même modélisation des flottants pour la preuve et pour

le calcul permet d"assurer que les propriétés établies en Coq sont préservées après extraction

(sous l"hypothèse que le mécanisme d"extraction vers OCaml de Coq est correcte). Une modélisation des flottants.Le standard IEEE-754 donne une définition très com- plète des nombres flottants qui convient parfaitement comme guide pour l"implémentation d"une

arithmétique flottante en machine. Néanmoins une représentation binaire est assez peu adaptée

7 Preuve formelle de propagateurs flottants A. Correnson, F. Bobot pour formaliser la notion de nombre flottant dans un assistant à la démonstration. Pour per- mettre à la fois des raisonnements formels plus simples sur les nombres flottants et des calculs effectifs au sein d"un assistant à la démonstration, la bibliothèque Coq Flocq [ 8 ] propose un compromis et fournit une implémentation des flottants comme des nombres de la formem2e.

Cette modélisation des nombres flottants est prouvée correcte vis à vis du standard IEEE-754

et peut être extraite vers un module OCaml fiable pour le calcul flottant. Ces propriétés font

donc de Flocq un outil de choix pour la suite des travaux présentés dans cet article. Opérateurs flottants.Flocq fournit un type flottantbinary_floatparamétré par une pré- cision et un exposant maximal (l"exposant minimal est déduit à partir de l"exposant maximal et de la précision tel que décrit dans le standard IEEE-754). Le typebinary_floatest défini comme un type algébrique avec un constructeur pour chacune des valeurs spéciales (NaN,0,

1) et un constructeur pour tous les flottants finis de la formem2e. Cette modélisation permet

de réduire les démonstrations en arithmétique flottante à une analyse de cas sur la forme des

flottants considérés.

Les opérateurs usuels paramétrés par un mode d"arrondi sont également fournis. Par soucis

de simplicité, nous omettrons les paramètres correspondant au format dans les échantillons de

code Coq et nous noterons simplementfloatpour désigner le type des flottants dans un format fixé. En suivant cette convention, on considère les opérateurs suivants : relations binairesBeqb, Bleb, Bltb : float -> float -> bool addition flottanteBplus : mode -> float -> float -> float constanteNaN NaN : float constantes infiniesB754_infinity : bool -> float projection dans les réelsB2R : float -> R opérateur d"arrondi générique

1round : mode -> R -> R

3.2 Monotonie : un réel problème de sémantique

Établir la preuve formelle d"un théorème en Coq est souvent une tâche longue et difficile, en

particulier lorsque les preuves impliquent de mobiliser des résultats d"arithmétique eta fortiori

d"arithmétique flottante. La preuve de correction d"opérateurs sur les domaine abstraits est très

consommatrice de ce type de résultats et en particulier de théorèmes de monotonie qui assurent

la préservation de la relationBlebà travers les opérations arithmétiques. Ces théorèmes sont

triviaux dansRmais plus difficiles à formuler voire même faux dans les flottants. La monotonie de l"addition réelle par exemple assure que8(x;y;z)2R3;xy!x+zy+z, mais la valeur

NaNne pouvant être comparée, il s"ensuit que ce résultat est faux dans les flottants. En effet, pour

x=1,y= +1,z= +1, on a bienxfymaisxfz=NaNet donc:(xfzfyfz).

Pour des raisons similaires, la plupart des résultats d"arithmétique flottante sont conditionnés

par des hypothèses spécifiques sur les opérandes. Ainsi la monotonie de l"addition dansFse ré-exprime de la façon suivante : Théorème 3.1(Monotonie de l"addition flottante).Soitmun mode d"arrondi etx;y;x0;y0

quatre flottants. Sixmfx06=NaN,ymfy06=NaN,xfyetx0fy0alorsxmfx0fymfy0.1. On pourrait s"attendre à ce qu"un opérateur d"arrondi soit de signatureR!F, mais une telle définition

ne serait pas calculable car les réels ne sont pas représentables en machine. En revanche, une axiomatisation des

réels suffit pour l"écriture de spécifications.quotesdbs_dbs28.pdfusesText_34

[PDF] complexité boucle for

[PDF] complexité algorithmique cours

[PDF] système de congruence exercice

[PDF] résoudre équation congruence

[PDF] exercice congruence

[PDF] théorème chinois pdf

[PDF] resoudre systeme congruence

[PDF] calcul consommation ampoule 100w

[PDF] consommation ampoule 60w

[PDF] combien coute une ampoule allumée

[PDF] calcul consommation ampoule led

[PDF] lumiere allumée toute la nuit consommation

[PDF] calcul de consommation électrique d'un appareil

[PDF] consommation ventilateur 40w

[PDF] consommation congelateur ancien