Calculs d'intervalles flottants (projet no. 3)

C possède deux types flottants: float et double. On suppose dans ce projet que tous les calculs sont faits en double (ce qui est souvent le cas), et que le type C double correspond exactement au type OCaml float.

Les flottants sont supposés obéir au format défini par la norme IEEE754. Ceci a un certain nombre de conséquences. D'abord, les flottants se découpent en deux catégories: les nombres flottants, et les NaN (``not a number''). Ces derniers représentent les résultats de calculs échoués comme 0.0/0.0 ou log (-1.0). Parmi les nombres flottants, on retrouve des nombres usuels comme 1.0, -2.34 ou 3.1415926535, mais aussi plus infini et moins infini. Attention, contrairement au cours [moins infini, 3.0] par exemple est l'intervalle qui contient tous les flottants £ 3.0, incluant moins infini!

Les infinis sont définis comme les constantes Arith.float_plus_infini et Arith.float_moins_infini. Vous pouvez tester si un float OCaml x est un Nan en appelant Arith.float_is_nan x.

On va représenter les flottants v par des couples (itv, nan), où itv est un intervalle (cf. intervalle.ml) de variation possible des valeurs de v lorsqu'elles parcourent les nombres flottants (y compris plus et moins infini!), et où nan est un booléen qui est vrai si et seulement si v peut valoir un NaN.

La difficulté principale de ce projet est de calculer correctement l'addition, la multiplication et la division. On notera les cas où des opérations arithmétiques retournent des NaN sont: l'addition de plus infini et de moins infini; la multiplication d'un infini par 0.0; la division de 0.0 par 0.0; la division d'un infini par un infini. Ceci constituera probablement l'essentiel de votre effort dans ce projet.

La fonction itv_float_convert_int est censée convertir un intervalle d'entiers en intervalle de flottants correspondant. Il s'agit de la fonction abstraite correspondant au cast (double)i, où i est un entier. On supposera que tous les entiers de tous les types entiers sont représentables exactement comme des double.

Quand aux fonctions de comparaison £, <, ==, noter que le résultat de n'importe quelle comparaison avec un NaN retourne toujours faux. (En particulier, et aussi surprenant que cela paraisse, x==x est faux lorsque x est un NaN.) On rappelle que faux est l'entier 0, vrai l'entier 1 en C.

This document was translated from LATEX by HEVEA.