ARC QUOTIENT: Utilisation certifiée de types concrets non-libres


QUOTIENT est une Action de Recherche Collaborative (ARC) de l'INRIA.

Résumé

Pour que l'équation ``programme = structure de données + algorithme'' rende totalement compte de l'activité du programmeur, il faudrait y ajouter l'équation ``structure de données = type de données + invariants'', équation à maintenir tout au long de l'écriture du programme et dont le maintien est encore peu instrumenté. Certains invariants comme ceux décrits par une notion de typage fort peuvent être garantis au moment de la compilation, ceux liés à l'existence de bornes peuvent être maintenus par l'insertion par le compilateur de vérifications faites à l'exécution. Lorsque les invariants sont plus compliqués, le programmeur ne reçoit que peu d'aide du compilateur. Par exemple, maintenir une structure de données sous une forme triée est en général entièrement à la charge du programmeur tout comme l'est le maintien de structures arborescentes sous forme de peigne droit. Le maintien de tels invariants doit être global à toutes les procédures constituant le programme, ce qui est source de nombreuses erreurs.

Or, beaucoup de ces invariants peuvent être exprimés par la donnée d'une relation d'équivalence sur une structure libre : une liste triée est un représentant bien choisi d'une liste modulo commutativité, un peigne droit est un représentant bien choisi d'un arbre binaire modulo associativité. Pour aider le programmeur souhaitant utiliser de tels invariants, il faut lui donner:

Ainsi, ayant décrit aisément son invariant, le programmeur sera entièrement débarrassé de la tâche de gestion de l'invariant, le compilateur lui refusant opportunément toute tentative de construction de ses données qui ne passerait pas par l'intermédiaire des fonctions de construction.

Il est aisé d'introduire des structures libres dès que l'on dispose d'une bonne notion de type, offrant des types produit et des types union. C'est le cas par exemple des types de la famille ML. Cela peut également se faire en Java à l'aide d'une bibliothèque de classes. Accumulés depuis plus de 30 ans, les travaux sur les théories équationnelles et la réécriture fournissent des résultats sur l'existence ou non de représentants canoniques de classes d'équivalence et sur le moyen de les construire effectivement. La proposition de projet QUOTIENT porte donc sur la définition d'une coopération entre ces deux paradigmes pour réaliser l'outil spécifié ci-dessus, permettant d'obtenir un ML ou un Java avec types quotients. Il a également pour but de certifier la correction des fonctions de constructions générées afin de permettre la preuve des programmes basés sur de tels types. Ce projet contribue ainsi au défi prioritaire de l'INRIA intitulé ``garantir la fiabilité et la sécurité des systèmes à logiciel prépondérant''.

Activités scientifiques envisagées

Notre projet a pour but d'étudier et de développer des outils pour un nouveau trait de programmation: les types concrets non-libres.

La plupart des algorithmes utilisent des structures de données avec des invariants, et l'ensemble des valeurs vérifiant ces invariants est souvent un ensemble de représentants pour les classes d'équivalence d'une certaine théorie équationnelle. Par exemple, une liste triée est un représentant particulier modulo commutativité. Les théories comme l'associativité, élément neutre, idempotence, etc. sont également très fréquentes.

Cependant, il n'y a quasiment aucun support pour construire et manipuler de tels types. La seule solution est d'utiliser un type abstrait ou un type concret avec constructeur privé et d'écrire à la main des fonctions de construction assurant l'invariant en calculant le représentant adéquat. Mais il n'existe aucun outil générant, pour un invariant donné, des fonctions de construction implantant cet invariant et les formules logiques décrivant les propriétés vérifiées par les valeurs de ce type. De plus, quand quelqu'un souhaite combiner différents invariants, il peut devenir très difficile de trouver un bon représentant et de l'implanter efficacement.

Dans le milieu des années 80, Simon Thompson a proposé un mécanisme dans le langage de programmation fonctionnel Miranda pour implanter de tels types. Cette proposition n'a pas marché en partie parce qu'aucun support n'était fourni pour vérifier que les invariants étaient correctement implantés et pour utiliser les propriétés des fonctions de construction.

Nous proposons donc non seulement de développer un outil générant, pour un invariant donné, des fonctions de construction et des formules logiques exprimant les propriétés des valeurs du type, mais également d'en certifier les résultats afin qu'ils puissent être utilisés dans des outils de preuve de programme.

Dans On the implementation of construction functions for non-free data types, Frédéric Blanqui, Thérèse Hardin et Pierre Weis ont montré comment certains résultats de la théorie de la récriture peuvent servir à définir des représentants et donc à vérifier la correction de fonctions de construction. C'est d'une certaine manière le point de départ de notre projet.

Nous détaillons maintenant les différents problèmes à résoudre:


statcounter Valid XHTML 1.1 Last updated on 3 September 2010. Come back to main page.