Introduction

Les méthodes formelles prennent une place de plus en plus grande dans le développement de logiciels. Dans leur revue sur l'état de l'art des méthodes formelles, Edmund Clarke et Jeannette Wing [18] écrivent :

The overarching goal of formal methods is to help engineers construct more reliable systems. Formal method is thus an area that cuts across almost all other areas in Computer Science. Its foundation lie squarely in mathematics, its intended applications are hardware and software systems, and its potential users are all developers involved in the system engineering process.

L'objectif du projet Lemme est de contribuer à l'application de ces méthodes à la construction de logiciels pour le calcul scientifique ¹.

Prouver la correction, même partielle, d'un programme qui réalise des calculs mathématiques suppose des activités variées :

• donner une représentation symbolique du programme, voire des algorithmes qu'il implémente.
• formaliser les propriétés qu'il doit vérifier, ce qui implique de disposer d'un langage capable de décrire naturellement les mathématiques utilisées.
• effectuer les preuves de ces propriétés.

Ces activités sont très liées, au moins par le fait qu'elles utilisent toutes les trois des représentations d'objets mathématiques (nombres, structures algébriques, fonctions, etc).

Elles ne sont pas forcément toutes automatisées, et peuvent ne pas utiliser les mêmes formalismes. Mais il est clair que plus elles seront traitées de manière homogène, plus les risques d'incohérence seront limités : parler des mêmes objets dans des modélisations différentes oblige à des précautions dans la cohérence des traductions.

Les expériences que nous avons menées depuis plusieurs années dans CROAP et SAFIR ont montré que la théorie des constructions inductives (CCI) développée par le projet Coq est un langage qui, quand on le parle à l'aide des logiciels Coq, Ocaml, et CtCoq, peut permettre de mener ces trois activités de front :

• Le système Coq, qui implémente le CCI, donne des outils pour effectuer des preuves (tactiques), et écrire des programmes fonctionnels (algorithmes et structures de données).

• Le langage Ocaml, dont le système de type, si on oublie les objets et les modules, est en gros un affaiblissement du CCI et joue un rôle de langage d'implantation pour les algorithmes écrits en Coq. En effet un processus automatique, l'extraction, permet de traduire simplement des programmes Coq en programmes Ocaml équivalents et efficaces dans leur exécution.

• Le système CtCoq, qui fournit un environnement graphique (basé sur Centaur actuellement, en cours de portage en Java dans l'environnement Aïoli), connecté à Coq, dans lequel on peut développer des preuves complexes à la souris (proof by pointing, drag and drop), manipuler des formules mathématiques à l'aspect naturel (symboles mathématiques, édition structurée, etc), et assurer la maintenance de grands développements de preuve.

L'algorithme de Buchberger [44] est l'exemple le plus complet que nous ayons traité en utilisant ces trois outils : à l'aide de CtCoq, l'algèbre des polynômes à plusieurs variables a été formalisée en Coq, l'algorithme de Buchberger y a été écrit, puis la preuve de sa correction a été faite. Enfin on a testé le programme Ocaml extrait sur des exemples significatifs, avec des temps de calcul intermédiaires entre les meilleurs programmes spécialisés et les logiciels de calcul formel généralistes comme Maple ².

Nous avons aussi traité d'autres exemples conséquents, comme l'algorithme de multiplication de Karatsuba, l'algorithme de Cantor-Zassenhaus de factorisation des polynômes dans les corps finis [30], l'algorithme de Stålmark pour la satisfiabilité des formules booléennes [29], un compilateur pour un langage impératif [8].

Notre approche est originale au sens où nous ne cherchons pas à prouver des programmes (au sens de programmes écrits dans un langage conventionnel comme C, Java, ou Caml), mais au contraire nous cherchons à produire des programmes conformes à leurs spécifications à partir de descriptions mathématiques ``usuelles'' des données, des algorithmes, et de leurs propriétés, ainsi que de leurs preuves. C'est ce dernier point qui nous semble original.

Un rêve serait de pouvoir par exemple écrire à la main sur tablette graphique l'algorithme de la transformée de Fourier rapide, les propriétés qu'elle vérifie, d'effectuer leurs preuves dans un style naturel en cliquant avec un stylet, et de traiter ensuite un exemple avec le programme Ocaml (ou Java) extrait...

Ou bien de développer sur le Web un cours de mathématiques de premier cycle utilisant les notations usuelles, avec des exercices et leurs solutions (preuves et calculs). ³

En quelques mots, nous cherchons à réduire la distance encore trop grande entre la résolution d'un problème mathématique (au sens large) sur le papier (ou au tableau) et les calculs sur ordinateur qu'il nécessite, en insistant sur la cohérence logique et le confort de ce passage de la théorie à la pratique.

Il n'est pas a priori dans nos buts de trouver des démonstrations nouvelles d'algorithmes mathématiques, ni d'en concevoir de nouveaux, ni encore d'en obtenir des implantations hyper-optimisées (d'autres le font très bien).

Nous partons plutôt d'une nécessité, qui est celle de la correction des programmes de calcul mathématique. Parmi les différentes voies possibles pour résoudre ce problème (on peut par exemple se concentrer sur l'arithmétique des ordinateurs, ou sur les preuves de propriétés de programmes Java), nous avons choisi non pas d'extraire les mathématiques des programmes, mais l'inverse, parce qu'il nous semble qu'avec les résultats dont nous disposons (CCI, Coq, CtCoq, Centaur, Aïoli) cette voie de recherche est raisonnable et prometteuse.