Changements de Représentation des Données dans le Calcul des Constructions

• Main Author: Magaud, Nicolas
• Language: FRE
• Published: Université de Nice Sophia-Antipolis 2003
• Subjects: [INFO:INFO_SE] Computer Science/Software Engineering; Outils d'aide à la preuve; théorie des types; <br />racine carrée; GMP; arithmétique en précision arbitraire; <br />types inductifs; transformation automatique de preuves
• Online Access: http://tel.archives-ouvertes.fr/tel-00005903; http://tel.archives-ouvertes.fr/docs/00/04/67/49/PDF/tel-00005903.pdf

Nous étudions comment faciliter la réutilisation des <br />preuves formelles en théorie des types. Nous traitons cette question <br />lors de l'étude <br />de la correction du programme de calcul de la racine carrée de GMP. <br />A partir d'une description formelle, nous construisons <br />un programme impératif avec l'outil Correctness. Cette description <br />prend en compte tous les détails de l'implantation, y compris <br />l'arithmétique de pointeurs utilisée et la gestion de la mémoire. <br />Nous étudions aussi comment réutiliser des preuves formelles lorsque<br />l'on change la représentation concrète des données. <br />Nous proposons un outil qui permet d'abstraire <br />les propriétés calculatoires associées à un type inductif dans<br />les termes de preuve.<br />Nous proposons également des outils pour simuler ces propriétés<br />dans un type isomorphe. Nous pouvons ainsi passer, systématiquement,<br />d'une représentation des données à une autre dans un développement<br />formel.