LIP6 2001/017
- Rapports de recherche
Fraction : analyseur de propriétés par des techniques de résolution de contraintes - F. Parrennes
- 14 pages - 25/06/2001- document en - http://www.lip6.fr/lip6/reports/2001/lip6.2001.017.pdf - 317 Ko
- Contact : Fabrice.Parrennes (at) nulllip6.fr
- Ancien Thème : SPI
- Mots clés : Analyse statique, vérification de propriétés, résolution de contraintes
- Directeur de la publication : David.Massot (at) nulllip6.fr
Ce papier décrit Fraction, un outil de vérification de propriétés de programme par utilisation de contraintes. L'utilisation de techniques liées aux contraintes pour vérifier des propriétés n'est pas véritablement nouvelle.
L'originalité de l'approche exposée est d'avoir défini une traduction d'un langage de style impératif en une série de systèmes de contraintes. Ce sont les algorithmes de résolution de contraintes qui permettent de valider ou non les propriétés recherchées. Cette traduction passe par une étape intermédiaire où l'on retrouve l'aspect fonctionnel des programmes.
L'utilisation du langage Ocaml a permis de réaliser facilement un prototype de la méthode dont l'architecture rappelle celle d'un compilateur. La définition d'un solveur de contraintes modulaire rend l'outil paramétrable par rapport à des modules de résolution de contraintes sur des domaines différents (les entiers et les booléens par exemple).
L'originalité de l'approche exposée est d'avoir défini une traduction d'un langage de style impératif en une série de systèmes de contraintes. Ce sont les algorithmes de résolution de contraintes qui permettent de valider ou non les propriétés recherchées. Cette traduction passe par une étape intermédiaire où l'on retrouve l'aspect fonctionnel des programmes.
L'utilisation du langage Ocaml a permis de réaliser facilement un prototype de la méthode dont l'architecture rappelle celle d'un compilateur. La définition d'un solveur de contraintes modulaire rend l'outil paramétrable par rapport à des modules de résolution de contraintes sur des domaines différents (les entiers et les booléens par exemple).