08/03/2001:
Sylvain Boulmé, Univ. Paris 6
Vers un environnement pour spécifier, programmer et certifier
(prouver) des bibliothèques de calcul formel.
Résumé
Le projet FOC du LIP6 développe un système pour
spécifier, programmer et certifier (prouver) des bibliothèques de
calcul formel. Je présenterai mes travaux de thèse autour de la
spécification du langage de bibliothèques de FOC.
Dans ce langage, chaque unité de bibliothèque représente une certaine
structure algébrique, comme les groupes, les anneaux, les algèbres de
polynômes, etc. En pratique, les bibliothèques de calcul formel
comportent un grand nombre de structures algébriques qui partagent
entre elles algorithmes, propriétés et preuves, de façon assez
compliquée. Par exemple, une notion calculatoire d'algèbre (comme le
pgcd) est définie par des propriétés algébriques. Toutes les
structures algébriques vérifiant ces propriétés partagent cette
notion. Mais chacune d'elles peut l'implanter en utilisant différents
algorithmes: génériques (communs à une large gamme de structures), ou
spécialisés (utilisant une représentation particulière des données, ou
communs à des structures vérifiant une certaine propriété).
Pour exprimer ce partage entre unités, l'utilisateur dispose de
mécanismes d'héritage. L'héritage permet de créer une unité à partir
de une ou plusieurs autres, en décrivant uniquement les différences de
l'unité créée vis-à-vis des unités héritées, tout en préservant leurs
propriétés. En effet, les algorithmes (et les preuves) applicables à
une unité A seront aussi applicables à une unité B qui hérite de
A. Par rapport aux mécanismes traditionnels de programmation orientée
objet, l'héritage est ici très restreint de manière à garantir la
cohérence logique des bibliothèques et la terminaison des programmes.
Ce langage a d'abord été spécifié en Coq. Il a ensuite été décrit de
manière abstraite (indépendament de toute syntaxe), dans un
métalangage catégorique, en s'inspirant des catégories contextuelles
introduites par Cartmell pour modéliser les types dépendants. Pour
donner lieu à des programmes exécutable, il est aussi proposé une
traduction de ces bibliothèques dans le langage Ocaml, en utilisant
divers traits de ce langage: polymorphisme, objets, modules, etc.