Description
Date depot: 1 janvier 1900
Titre: Un outil de vérification formelle pour la modélisation de mathématiques effectives
Directrice de thèse:
Catherine DUBOIS (CEDRIC)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Le langage Focal [2], initialement conçu par T. Hardin et R. Rioboo, permet de construire incrémentalement des applications certifiées, en partant de spécifications abstraites, appelées espèces, jusqu'à des implantations concrètes formellement vérifiées, appelées collections. Ces différentes structures peuvent être combinées en utilisant l'héritage et la paramétrisation, inspirés de la programmation orientée objet. De plus, chacune de ces structures est équipée d'un ensemble support, appelé représentation, à la manière des spécifications algébriques. Dans ce langage, il y a une séparation nette entre les activités de programmation et de preuve : un compilateur [7] est capable de produire du code OCaml pour l'exécution et du code Coq pour la certification. En outre, Focal possède un outil de preuve automatique dédié, appelé Zénon [3]. Une nouvelle version du compilateur, appelé focalize, a été récemment distribuée et est disponible à l'adresse http://focalize.inria.fr/.
Actuellement, Focal possède une visibilité assez importante dans le domaine des méthodes formelles, de part la diversité des développements réalisés, mais aussi en raison de la stabilité des langages vers lequel il est compilé (OCaml et Coq, développés depuis plus de 20 ans par l'Inria). Entre autres applications, on notera une bibliothèque certifiée de Calcul Formel (distribuée avec le compilateur), mais aussi des formalisations concernant des réglementations de la sûreté de l'aviation civile [4], des politiques de sécurité [6], et plus récemment, des modèles de systèmes à base de composants [1]. Tous ces développements tendent à montrer que Focal est un langage de spécification général, aussi bien adapté aux mathématiques qu'à des applications du monde réel.
Ce sujet de de thèse s'inscrit dans une problématique applicative forte, consistant à produire un environnement Focal suffisamment complet pour permettre la modélisation de mathématiques effectives. En effet, comme dit précédemment, une bibliothèque conséquente de Calcul Formel (environ 10000 lignes de code) a été développée en Focal, et outre d'excellents résultats en termes de performance, ce développement a surtout permis de mettre en évidence certaines limitations du langage de spécification de Focal.
Parmi ces limitations figurent l'impossibilité d'écrire des espèces récursives (cette limitation apparaît lorsque l'on souhaite modéliser les polynômes récursifs par exemple), ou l'absence d'invariants pour une espèce (ce problème est notamment soulevé lorsque l'on souhaite développer des quotients). Toutes ces limitations témoignent du fait que la modélisation de mathématiques effectives implique la possibilité de réaliser des spécifications très abstraites, et que ces spécifications abstraites nécessitent une forte expressivité du langage. Toute la difficulté dans le cadre de Focal est de permettre cette grande expressivité tout en contrôlant qu'elle n'introduit pas
d'incohérences dans la théorie sous-jacente.
Ainsi, un des premiers objectifs de cette thèse est d'introduire les extensions nécessaires au langage de spécification de Focal pour pallier les limitations mises en évidence lors du développement de la bibliothèque de Calcul Formel. Il s'agit non seulement de construire ces extensions, mais aussi de les fonder sémantiquement et formellement. Cette fondation sémantique et formelle devra être réalisée dans le cadre théorique d'une sémantique opérationnelle de Focal (car plus proche d'une implantation et du compilateur en particulier), et un travail préalable consistera à étendre les travaux de S. Fechter [5], afin que le modèle sémantique puisse prendre en compte non seulement les aspects calculatoires (exécution), mais aussi les propriétés et les preuves (certification). Ensuite, une fois ces extensions validées et dans une optique plus pratique, il s'agira d'intégrer concrètement ces extensions au compilateur existant de Focal.
Un autre objectif de cette thèse consistera à continuer de développer la bibliothèque de Calcul Formel de Focal, et en particulier, les parties de la bibliothèque qui ont fait apparaître des limitations du langage de spécification et qui ont nécessité des extensions du compilateur. Ainsi, dans un premier temps, on pourra notamment se concentrer sur le développement des polynômes récursifs et celui des quotients (qui ont introduit les limitations identifiées précédemment), puis dans un deuxième temps, il sera possible d'aborder des problèmes plus complexes permettant de valider l'expressivité du langage de spécification.
Doctorant.e: Tollitte Pierre-Nicolas