Soutenance mémoire
Lambda-calcul
Le lambda-calcul, inventé par Church, est avant tout une formalisation de l’écriture des fonctions. On écrira par exemple λx.λy.x la fonction qui prend deux arguments (x et y) et qui renvoie comme résultat le premier (la valeur de x). Un terme du lambda-calcul est soit une variable, soit l’application de deux termes (notée par la juxtaposition) f x signifiant “f appliqué à x”, et l’abstraction d’une variable λx.t signifiant “la fonction qui à x associe t”, où x peut apparaître dans t. On ajoute à cela des parenthèses pour lever les ambiguïtés. Cette notation ne serait pas très utile sans la règle de calcul qui lui est associée : la bêta-réduction. Cette règle de calcul est purement syntaxique. Elle exprime qu’un terme de la forme (λx.t) u (la fonction qui à x associe t, appliquée à u), se calcule en t, dans lequel on aura substitué u à chaque occurrence de x. Par exemple, (λx.λy.x) t1 t2 donne d’abord (λy.t1) t2, puis t1 (si y n’apparaît pas dans t1). À travers des codages, il est possible d’exprimer des données et les opérations sur ces données. Par exemple, on codera le 0 par λx.λf.x, le 1 par λx.λf.(f x), le 2 par λx.λf.(f(f x)), etc. Le lambda-calcul étant en fait “trop expressif” (on peut appliquer n’importe quelle fonction, voire quelque chose qui n’est pas une fonction, à n’importe quoi), il est possible de le typer, c’està-dire de déterminer le type d’un terme de façon à savoir d’une part s’il est correct, d’autre part dans quel contexte l’utiliser. Cela permet de restreindre le langage à une certaine classe de fonctions (par exemple les fonctions totales). On écrira par exemple λ(f : ι → ι)λ(x : ι).(f x) (où ι est un type arbitraire) est une fonction prenant en argument f (une valeur fonctionnelle) et x et renvoyant le résultat de l’application f x, lui même de type ι. On ne pourra par plus écrire x x (x appliqué à lui-même), car on ne saura pas le typer. Deux grandes familles de méthodes existent pour typer le lambda-calcul : à la Church, en contraignant les variables par un type (comme ci-dessus), ou à la Curry, en cherchant à déterminer le type sans que le terme soit annoté.
Raffinement
Le raffinement est issue des travaux d’axiomatisation des langages de programmation de Morgan [45] et Dijkstra [25]. Contrairement à la méthode précédente, celle-ci est beaucoup plus adaptée au traitement des programmes impératifs. Comme pour l’extraction, on part de la spécification formelle, mais cette fois, on cherche à “raffiner” cette spécification en passant par des états intermédiaires (des spécifications intégrants des parties de programme ou vice-versa), jusqu’à atteindre un programme vérifiant cette spécification. On ne passe donc pas directement de la spécification au programme définitif, mais plutôt de pseudo-programme en pseudoprogramme, les premiers ressemblants beaucoup à la spécification, chaque étape introduisant de plus en plus de déterminisme, jusqu’à arriver à des programmes annotés par quelques propriétés, puis au programme final. Chacune de ces étapes engendrera des obligations de preuves, permettant de garantir que l’étape n + 1 satisfait bien ce qui est requis à l’étape n. Les représentations des données et les algorithmes seront de plus en plus précis. Alors que l’extraction de programme consiste en partie à faire le tri entre ce qui dans une preuve relève du contenu algorithmique et le reste que l’on “oublie”, dans le raffinement, le contenu algorithmique est introduit petit-à-petit par l’utilisateur du système, tandis qu’il fait disparaître la spécification. Le principal système faisant appel au raffinement est la Méthode B de J.-R. Abrial, qui combine cette technique avec une méthodologie de génie logiciel dans une formalisation en théorie des ensembles [2].
Coq
Le système Coq est développé depuis 1986 à l’INRIA. Il est dû à l’origine à Thierry Coquand et Gérard Huet [62], et a profité de nombreuses contributions. Ce système est basé sur le calcul des constructions inductives [65], une extension du lambda-calcul typé, comprenant les types récursifs, le polymorphisme de type, ainsi que le produit et la somme “dépendants”, c’est-à-dire dont le deuxième argument peut dépendre du premier. Un exemple de type dépendant (d’un entier) est le type “être une liste de longueur n”. La richesse du système de type de Coq est nécessaire : dans le calcul des constructions on assimile types et formules (types as formulae [20, 31]) et la preuve d’un énoncé est un terme dont le type est l’énoncé démontré. Dans Coq, tout est codé dans ce calcul : aussi bien les termes, que les formules, les preuves ou les types. . . La logique utilisée est d’ordre supérieur, et elle est intuitionniste (n’utilise pas le tiers exclu). Coq est un système qui permet l’extraction de programme à partir d’une preuve. Dans ce système, la preuve d’une proposition de la forme “pour tout x de type τ , il existe y de type τ0 tel que la proposition Φ(x, y) est vraie” est une fonction prenant en argument un x de type τ et retournant un témoin y de type τ0 et une preuve Π que y vérifie bien cette propriété. Dans le cadre de l’extraction de programme (cf. section 1.2.2.1), on n’est intéressé que par la valeur de retour y, et non par la preuve : dans Coq, on distinguera donc les propositions ayant un contenu algorithmique (dont la preuve permet de construire y), celles-ci seront de type Set, des propositions sans contenu algorithmique (dont la preuve permet de construire Π), qui porteront le type Prop. L’extraction oublie la preuve de tout ce qui est de type Prop pour ne conserver qu’une fonction (la preuve de ce qui est de type Set) qui à x va associer y. Le codage dans le calcul des constructions inductive a pour avantage d’être uniforme, mais pour inconvénient de n’être pas naturel pour l’utilisateur. En effet, le calcul des constructions est un système riche, mais complexe, et l’utilisateur ne peut jamais oublier qu’il travaille dans ce système. En ce qui concerne les définitions, déclarations, etc. on utilise un langage étendu permettant de construire les objets de façon plus simple et avec un langage plus riche que le calcul des constructions (bien que tout soit traduit vers celui-ci). Pour les preuves, l’objectif est de construire le terme de preuve, mais l’utilisateur est aidé par des tactiques plus ou moins automatisées de “granularité” supérieure au calcul des constructions. Comme la preuve est traduite en un terme du calcul, elle peut être validée (une fois terminée) par une partie de faible taille du système, et cette validation est une simple vérification de type (le type d’une preuve étant l’énoncé qu’elle prouve). La sûreté du système repose donc sur cette vérification du type du terme de preuve. L’interface de Coq est une boucle d’interaction de type “ligne de commande”, cependant d’autres interfaces ont été conçues pour communiquer avec le système. On notera particulièrement Proof General [3] qui est une interface générique réalisée comme extension de l’éditeur de texte XEmacs [67], qui peut être adaptée à d’autres systèmes de preuve en ligne de commande et qui se rapproche d’une édition pleine page. D’autres interfaces ont aussi été implémentées pour Coq, notamment PCoq ou son ancêtre Ct-Coq, de Yves Bertot et Laurent Théry [63], qui ont une approche “prouver en cliquant”, c’est-à-dire mettant en avant l’ergonomie et l’utilisation de la souris pour l’utilisation de systèmes d’aide à la preuve.
PhoX
PhoX, développé par Christophe Raffalli [55] est basé sur une logique d’ordre supérieure, inspirée par l’Arithmétique Fonctionnelle d’ordre 2 (AF2) de Jean-Louis Krivine (lambda-calcul, égalité et définitions de types inductif voir [34]). PhoX étend donc AF2 à l’ordre supérieur, et ajoute des constructions pour simplifier les définitions inductives. Les preuves se font sur le même principe que pour la plupart des autres systèmes : on travaille sur des séquents avec des règles basées sur la déduction naturelle et le calcul des séquents. Une particularité de PhoX est que, de manière similaire à la déduction naturelle, les règles peuvent être classées en règles d’introduction (celles qui, si l’on regarde la preuve des hypothèses vers la conclusion, permettent d’introduire un connecteur ou une constante), règles d’élimination (l’inverse, qui comprend les règles combinant une hypothèse avec le but courant), et règles de réécritures. PhoX généralise cela en permettant de créer de nouvelles règles intro et elim ou rewrite à partir des théorèmes montrés par l’utilisateur. Cela offre l’avantage pour celui-ci de pouvoir taper la commande intro, par exemple, et le système déterminera laquelle utiliser parmi sa base de commandes d’introduction répertoriées. Cela permet d’avoir une tactique automatique capable d’utiliser la récurrence (c’est une règle d’élimination), ainsi que les lemmes de l’utilisateur en fonction de la catégorie dans laquelle il les a rangé. PhoX construit des termes de preuve, mais ne les exporte pas.
|
Table des matières
Introduction
1 Les systèmes d’aide à la preuve
1.1 Qu’est-ce qu’un assistant de preuve ?
1.1.1 Notions préliminaires
1.1.1.1 Variables et fonctions
1.1.1.2 Prédicats et types
1.1.1.3 Termes et formules
1.1.1.4 Preuves
1.1.1.5 Lambda-calcul
1.1.1.6 Isomorphisme de Curry-Howard
1.1.2 Généralités
1.1.3 Interaction
1.1.4 Ingrédients
1.2 Pour l’informatique
1.2.1 Spécification
1.2.2 Implémentation
1.2.2.1 Extraction
1.2.2.2 Raffinement
1.2.3 Vérification
1.3 Tour d’horizon de quelques systèmes
1.3.1 Coq
1.3.1.1 Exemple
1.3.1.2 Interface
1.3.1.3 Program
1.3.2 Agda et Alfa
1.3.3 Isabelle/HOL
1.3.4 PhoX
1.3.5 PVS
1.3.6 ACL2
1.3.6.1 Exemple
1.4 Synthèse
1.5 Conclusion
2 Motivations de ce travail
2.1 ML comme langage cible
2.2 Pourquoi et pour qui ?
2.3 Vérification de programme
2.4 Une logique simple
2.5 Un système extensible, mais sûr
2.6 Un système ergonomique
2.7 Objectifs
3 Formalisation
3.1 Quelques notations
3.2 Définition du langage miML
3.2.1 Syntaxe
3.2.2 Langage de types
3.2.3 Typage des termes
3.2.4 Évaluation
3.3 Langage de spécification
3.3.1 Formules
3.3.2 Typage des formules
3.3.3 Système de preuve
3.4 Théorie
3.4.1 Compléments sur les types
3.4.2 Égalité
3.5 Langage Vernaculaire
3.5.1 Déclaration
3.5.2 Définition
3.5.3 Axiome
3.5.4 Théorème
3.5.5 Let
3.5.6 Type
3.5.7 Session
3.6 Conclusion
4 Spécification
4.1 Modèle client-serveur
4.2 Protocole de communication
4.2.1 Classe Protocol
4.2.1.1 Requêtes
4.2.1.2 Réponses
4.2.2 Classe Session
4.2.2.1 Requêtes
4.2.2.2 Réponses
4.2.3 Classe Proof
4.2.3.1 Requêtes
4.2.3.2 Réponses
4.3 Spécification du moteur de preuves
4.3.1 Environnement
4.3.2 Preuves
4.3.3 Niveau session
4.3.4 Niveau preuve
4.4 Spécification de l’interface
4.4.1 Niveau session, événements utilisateur
4.4.2 Niveau session, événements moteur
4.4.3 Niveau preuve, événements utilisateurs
4.4.4 Niveau preuve, événements moteur
5 Implémentation
5.1 Généralités
5.2 Utilitaires
5.3 Identificateurs, noms et contextes
5.4 Types, termes et formules
5.5 Gestion des entrées
5.6 Preuves
5.6.1 Raffinement
5.6.2 Représentation
5.6.2.1 ProofTree
5.6.2.2 ProofStep
5.6.2.3 ProofGoal
5.6.2.4 ProofRule
5.6.2.5 ProofTac
5.6.2.6 Termes de preuves
5.7 Session
5.8 Communication et initialisation
5.9 API
5.10Tactiques
5.11Remarques
6 Résultats
6.1 État actuel
6.1.1 Ce qui a été fait
6.1.2 Ce qui manque
6.2 Difficultés rencontrées
6.2.1 Contextes, noms et identificateurs
6.2.2 Traitement de l’égalité et de l’évaluation
6.3 Comparaison avec d’autres systèmes
6.4 Utilisation
6.4.1 Termes
6.4.2 Formules
6.4.3 Vernaculaire
6.5 Règles et tactiques
6.5.1 Règles
6.5.1.1 Déduction libre enrichie
6.5.1.2 Autres règles
6.5.2 Tactiques
6.5.2.1 Pour l’utilisateur
6.5.2.2 Pour l’automatisation
6.6 Remarque sur l’écriture des tactiques
6.7 Interface toplevel
6.8 Exemple
6.8.1 Tri par insertion
6.8.2 Types, fonctions et lemmes de base
6.8.3 Insertion et tri
6.8.4 sort renvoie une liste triée
6.8.5 sort préserve les éléments de la liste
6.8.6 Arithmétique et manipulations d’arbre
6.8.6.1 Arithmétique
6.8.6.2 Opérations sur les booléens
6.8.6.3 Évaluateurs
6.9 Conclusion sur les exemples
Conclusion
A Introduction de l’implication
Télécharger le rapport complet
