Précédent : Modèles opérationnels des langages de Remonter : Fondements scientifiques Suivant : Une application au commerce électronique
Précédent : Modèles opérationnels des langages de
Remonter : Fondements scientifiques
Suivant : Une application au commerce électronique
Participants :
Jean Duprat, Daniel Hirschkoff, Frédéric Prost
Mots clés : Ramasse-miettes, algorithmique distribuée, analyse statique, non-interférence, modularité, PTS, bibliothèques de preuves, théories mathématiques .
Nous nous attachons à traduire en Coq des démonstrations ayant donné lieu à des publications dans des domaines variés de l'informatique. Notre premier travail important fut l'écriture de la preuve de correction d'une solution au problème de synchronisation d'une ligne de fusiliers parue en 1987 dans Theoretical Computer Science sous le titre «A six-state minimal time solution to the firing squad synchronization problem» par J. Mazoyer.
Le travail successif a porté sur un algorithme distribué de ramasse-miettes imaginé par L. Moreau. Cet algorithme met en jeu une machine abstraite composée d'automates d'états finis (sites) communiquant entre eux par messages. Cette machine évolue dans le temps de façon non déterministe par transitions choisies dans un ensemble fini de transitions possibles. La modélisation des liens de transmission des messages entre sites se fait par files d'attente. La preuve de sûreté met en évidence des invariants tenant compte du nombre de messages d'un type donné dans une file d'attente ou dans une famille de files d'attente et d'informations contenues dans des tables internes à chaque site. L'écriture de la preuve en Coq a été achevée, en collaboration avec Luc Moreau (Université de Southampton, Royaume Uni). Ce travail a permis de clarifier la preuve et de préciser davantage les spécifications de la machine abstraite servant de support d'exécution à l'algorithme.
Par ailleurs, Jean Duprat a encadré le stage d'un étudiant de première année du Magistère Informatique et Modélisation de Lyon: Clément Renard. Le sujet était la recherche des meilleures formalisations des graphes en Coq pour faciliter l'écriture de preuves en théorie des graphes. Il semblerait que, à l'inverse d'une écriture mathématique dans laquelle une formulation minimaliste est généralement recherchée, l'introduction bien choisie de redondances d'informations simplifie l'écriture de preuves. Ce travail doit être poursuivi.
Une des limitations des méthodes formelles telles que l'extraction de programmes à partir de preuves de leurs spécifications vient de l'inefficacité des programmes produits. Afin d'amélirorer la qualité de ces programmes il est nécessaire des les analyser pour pouvoir les optimiser. Comme dans de tels systmes on possède l'arbre de typage d'un programme, il semble naturel d'essayer d'en tirer parti pour l'analyse. L'utilisation de systèmes de types non standards (avec annotations), est bien connue dans la communauté des langages de programmation fonctionnelle. Pourtant ces types se comportent «mal» dans des logiques d'ordre supérieur (systme F, Calcul des Constructions par exemple) : on ne sait pas très bien comment s'interprètent les annotations dans des systèmes avec types dépendants ou encore polymorphisme. L'effort entrepris dans cet axe de recherche a pour but de mieux comprendre le sens de ce genre d'analyses, en particulier dans l'espoir de généraliser celles-ci aux systèmes de types purs.