GhostML un petit langage avec du code fantôme

Télécharger le fichier pdf d’un mémoire de fin d’études

Méthodes formelles

Les approches et les techniques que l’on qualifie de méthodes formelles partagent la même idée de modéliser le comportement d’un programme à l’aide des concepts mathématiques dans le but de montrer la correction d’un programme vis-à-vis de sa spécification. Il existe de nombreuses approches formelles, basées sur des formalismes différents. On peut citer notamment la vérification de modèles (en anglais model checking), l’interprétation abstraite, le raffinement, l’utilisation des systèmes de types et la vérification déductive des programmes. Parmi toutes les approches formelles, on peut distinguer celles qui s’appuient sur une analyse statique : cela veut dire que, contrairement au test, ces approches visent à établir la correction d’un programme, sans exécuter son code. L’idée de ces approches est que, lorsque l’on est capable de donner une description mathématique d’un langage de programmation (typiquement, en termes d’une sémantique formelle, par exemple, une sémantique opérationnelle, dénotationnelle, par un ensemble d’équations, etc.), il devient possible de connaître précisément ou, du moins, d’approximer le comportement de chaque instruction sans avoir besoin de l’exécuter. Pour un aperçu détaillé du panorama des méthodes formelles, le lecteur pourra consulter par exemple les ouvrages de Monin et Aleida et al. En ce qui concerne cette thèse, ce sont les deux dernières approches formelles mentionnées, le typage et la vérification déductive, qui nous intéressent particulièrement, la vérification déductive étant le contexte général de notre travail et le typage étant notre outil principal. Avant de passer à la problématique et aux contributions de cette thèse, nous présentons brièvement ces deux approches.

Systèmes de types

Un système de types est une forme d’analyse statique utilisée pour montrer, le plus souvent d’une manière décidable, l’absence d’une certaine catégorie d’erreurs bien définie, en classifiant les phrases de programme selon les types de valeurs qu’elles représentent. Explicitons certains points de cette définition un peu succincte.
Le premier aspect important du typage concerne l’utilisation des types en tant qu’objets syntaxiques. Cela signifie simplement que le typage manipule explicitement des classifications que le programmeur garde généralement en tête ou laisse en commentaires.
Par exemple, une expression entière comme 5+42 va avoir le type int, une expression booléenne 42 < 42 va avoir le type bool, une fonction fib qui calcule les nombres de Fibonacci va avoir le type int æ int, etc. En utilisant les informations sur les types uniquement, le système vérifie alors la cohérence de l’utilisation des types dans les expressions composées, telles que les appels de procédures, les instructions de contrôle, etc., selon un ensemble de règles de typage où chaque règle décrit le typage d’une catégorie syntaxique donnée. Sans rentrer dans les détails techniques, insistons sur le caractère compositionnel des règles du typage : pour qu’une expression donnée soit bien typée, il faut que toutes ses sous-expressions soient bien typées et que leurs typages soient cohérents entre eux. Par exemple, dans une conditionnelle de la forme if b then e1 else e2, il est raisonnable de la typer selon la règle que b doit avoir le type bool et que les expressions e1 et e2 de chaque branche doivent avoir le même type. De même, dans un appel de fonction comme f 42 true, il est raisonnable de la typer selon la règle que le type de chaque argument factuel doit être le même que celui du paramètre formel correspondant, c’est-à-dire que le type de f doit être int æ bool æ · .
L’intérêt de manipuler les types explicitement est que les expressions d’un programme qui n’ont aucun sens calculatoire comme 1+fib, 42 true, etc., vont alors être rejetées par le typage comme erronées, car elles ne respectent aucune règle du typage.
Un autre aspect du typage important est qu’il peut être considéré non seulement comme outil d’analyse statique, mais qu’il peut faire l’objet d’une étude théorique.
C’est d’ailleurs l’aspect du typage qui nous importe certainement le plus ici, car le but de cette thèse est d’explorer des solutions qu’une approche à base de systèmes de types peut apporter à la vérification des programmes. Plus spécifiquement, chaque fois que nous allons étudier un système de types, nous allons procéder en trois temps : d’abord, nous donnons la syntaxe abstraite et la sémantique opérationnelle d’un langage de programmation ; ensuite, nous équipons ce langage par un système de types caractérisé par un ensemble des règles de typage ; et enfin, nous montrons la correction du typage, c’est-à-dire que les programmes bien typés ont les propriétés qui nous intéressent.
Remarquons que pour montrer la correction du système des types nous allons utiliser l’approche syntaxique de Wright et Felleisen [44] où une sémantique opérationnelle à petits pas, définie inductivement comme une relation entre des configurations de départ et une configurations d’arrivée, décrit toutes les manières possibles de réaliser un pas d’évaluation, ce qui permet de montrer la correction du typage par induction sur la relation d’évaluation.
Enfin, il peut paraître au lecteur comme trop restrictif qu’un système de types a pour objectif de montrer l’absence non pas de tous les bugs, mais seulement d’une certaine catégorie. Néanmoins, on comprend mieux l’importance et les enjeux pragmatiques derrière le typage, lorsque l’on considère le caractère décidable de la plupart des systèmes de typage utilisés en pratique. En effet, suite aux travaux de Gödel, Church et Turing, dans les années trente du dernier siècle, on sait que la décidabilité et la complétude sont deux choses irréconciliables. Cela a pour conséquence que, pour tout langage de programmation quelque peu réaliste, trouver toutes les erreurs d’exécution possibles est un problème indécidable, c’est-à-dire qu’il n’existe pas d’algorithme qui permettrait de décider en temps fini si un programme arbitraire est correct ou pas. Or, lorsque l’on renonce à la complétude, on retrouve alors la possibilité de concevoir un algorithme qui décide si un programme est exempt ou pas de certains types d’erreurs. On comprend mieux maintenant pourquoi des langages de programmation comme Java, C, C++, OCaml sont tous équipés d’un système de types : un grand nombre d’erreurs peuvent être détectées automatiquement par le typage pendant la phase de compilation, en avertissant le programmeur par un message instructif sur l’endroit et l’origine des erreurs trouvées.
Enfin, notons que nous n’abordons pas ici de nombreux aspects du typage en soit très importants mais orthogonaux à notre propos, tels que la correspondance Curry- Howard, l’inférence de types, le sous-typage, la théorie des types dépendants, etc.
Le lecteur intéressé pourrait consulter l’excellent ouvrage « Types and Programming Languages » de Benjamin Pierce [37, 38] .
Comme nous venons de le remarquer, le typage renonce de la complétude au profit de la décidabilité. Nous présentons maintenant brièvement la vérification déductive de programmes, une méthode formelle qui, bien que plus coûteuse qu’un test et moins décidable que le typage, peut apporter un degré maximal de confiance dans la correction d’un programme.

Vérification déductive des programmes

L’idée clé de la vérification déductive est en fait très simple : puisque, intuitivement, un programme correct est un programme qui fait exactement ce qu’il est censé faire selon les intentions du programmeur, il suffit, d’une part, de rendre ces intentions explicites dans un langage mathématique et, d’autre part, d’exprimer la correction d’un programme par un ensemble d’énoncés mathématiques lesquels, lorsqu’ils sont vrais, impliquent la correction du programme vis-à-vis des intentions de l’utilisateur.
La figure 1.2 représente ces trois étapes de la vérification déductive schématiquement.
La première question est de savoir quelle est la manière adéquate pour exprimer l’interaction entre la spécification et l’ensemble des instructions d’un programme. Une première tentative d’élever les idées de Turing au rang d’un cadre formel, dans lequel on pourrait raisonner sur la correction de programmes d’une manière systématique, a été faite par Floyd [25] dans son travail Assigning meaning to programs. L’interaction entre la spécification et le code est exprimée à l’aide des organigrammes, mais l’idée reste celle de Turing : à chaque instruction on associe une condition qui doit être vraie avant que l’exécution soit exécutée et une assertion qui doit être vraie après l’exécution si la condition initiale a été respectée. En faisant une preuve par induction sur le nombre d’instructions exécutées, il devient alors possible de démontrer des propriétés du programme de la forme : « si les valeurs initiales des variables et des arguments en entrée satisfont une propriété R1, alors les valeurs des variables et le résultat en sortie satisfont une propriété R2 ». Par ailleurs, la preuve de terminaison du programme devient possible : il suffit de montrer qu’une mesure décroît strictement et d’une manière finie à chaque transition possible dans le flot de contrôle du programme. Mais c’est surtout le travail de Hoare An axiomatic basis for computer programming [26], paru deux ans après celui de Floyd, qui a donné à la vérification déductive le cadre formel que l’on utilise encore aujourd’hui et que l’on appelle la logique de Hoare.
Le concept de base de cette logique consiste à incarner les idées de Turing à l’aide des triplets de la forme { P } s { Q } qui relient l’instruction de programme s, la précondition P et la post-condition Q.
Un tel triplet est valide si et seulement si l’exécution de l’instruction s dans un état quelconque qui satisfait les propriétés de la précondition P résulte en un état qui satisfait les propriétés de la post-condition Q. La correction de programme peut être alors obtenue en assemblant les triplets de chaque instruction selon les règles d’inférence qui décrivent les formes possibles des triplets valides pour chaque construction du langage. En procédant de cette manière-là, l’énoncé mathématique qui se porte garant de la correction d’un programme devient simplement la validité du triplet { P } S { Q } où S correspond au programme en entier, P est l’ensemble des hypothèses sur les entrées et l’état avant son exécution et Q constitue les propriétés que l’on souhaite démontrer pour la valeur et l’état final de l’exécution.
La logique de Hoare permet de poser un cadre formel pour construire les conditions de vérifications de l’énoncé de correction, mais elle ne fournit pas de méthode efficace pour le faire. En effet, il est possible d’appliquer les règles de Hoare à chaque instruction de programme, en construisant pas à pas la dérivation du triplet pour le programme en entier, mais cela nécessite de donner toutes les pré- et des post- conditions des triplets intermédiaires. Cette manière de procéder est trop fastidieuse pour construire l’énoncé de correction de programmes même relativement petits. La deuxième question est donc de savoir comment construire l’énoncé de correction d’une manière plus efficace. La réponse à cette question a été apportée en 1975 par Dijsktra [21] qui y a introduit le calcul de plus faibles préconditions, une technique qui a permis d’apporter beaucoup d’automatisation dans le processus de la construction de l’énoncé de correction.
L’observation de Dijsktra était que seulement certains endroits dans le programme nécessitent que l’utilisateur écrive des assertions logiques intermédiaires (typiquement, les boucles), les assertions de la plupart des triplets intermédiaires pouvant être inférées et combinées d’une manière automatique. Partant de cette observation, l’idée de Dijsktra est de calculer récursivement, à partir du programme S et la post-condition Q, une précondition wp(S,Q) qui exprime la plus faible condition logique sur les états initiaux de l’exécution de S telle que les états finaux vérifient la post-condition Q.
L’énoncé de correction pour le programme S est alors exprimé par une implication P =Δ wp(S,Q)
Le calcul de plus faibles préconditions de Dijkstra permet ainsi de construire des conditions de vérifications d’une manière efficace et automatisable. Cependant, pour prouver un programme, il reste à démontrer l’énoncé mathématique de sa correction.
La troisième question est donc de savoir quelles sont les approches plus efficaces que sortir une feuille de papier et un crayon pour faire la preuve. Une approche possible est d’utiliser des assistants de preuve tels que Coq [9], Isabelle [28] ou PVS [36], ce qui apporte un degré de confiance inégalé dans la preuve, mais demande toujours à l’utilisateur de mener lui-même le raisonnement. Cependant, on peut remarquer qu’une grande partie des conditions de vérification concernent les propriétés de sûreté (l’absence de débordement des calculs arithmétiques, l’accès aux tableaux à l’intérieur des bornes, etc.) pour lesquelles la preuve automatique devient envisageable. D’autre part, les démonstrateurs automatiques ne cessent d’être perfectionnés, et permettent de résoudre des problèmes de plus en complexes, au moins pour certaines théories bien définies. On peut citer notamment les démonstrateurs automatiques de la famille des solveurs SMT (Satisfiability Modulo Theory) tels que Alt-Ergo [11], CVC3 [6], Z3 [19].
À l’aide de ces démonstrateurs, il devient possible de prouver automatiquement la correction, y compris la correction fonctionnelle, des programmes aussi complexes que l’algorithme de Strassen de multiplication des matrices [17] ou l’algorithme de Koda-Ruskey de génération des idéaux d’une forêt d’arbres partiellement ordonnées [24].
Bien entendu, pour que le processus de la vérification déductive devienne l’objet d’une technologie, il faut concevoir un outil de vérification qui permette à l’utilisateur d’effectuer chacune des trois étapes résumées dans la figure 1.2. C’est exactement ce qui est fait dans les plateformes de vérifications telles que Boogie [5] et Why3 [23].
Comme le travail de cette thèse concerne directement Why3, nous en donnons d’abord un bref aperçu et un exemple de son utilisation, avant de présenter les contributions de cette thèse.

L’outil de vérification Why3

Why3 est une plateforme de vérification qui donne accès à un ensemble d’outils permettant à l’utilisateur d’implémenter, spécifier formellement et prouver des programmes à l’aide de nombreux démonstrateurs automatiques tels que Alt-Ergo [11], CVC3 [6], z3 [19] etc., et interactifs tels que Coq [9], Isabelle [28] et PVS [36]. Pour cela, Why3 dispose d’un langage de programmation et de spécification, appelé WhyML [23], qui présente de nombreuses similarités avec des langages fonctionnels de la famille ML, telles que du filtrage par motif, des définitions de types algébriques, du polymorphisme et l’inférence de types à la Hindley-Minler, mais aussi des traits impératifs comme la modification de l’état mémoire ou des exceptions.
La correction fonctionnelle des procédures peut être spécifiée au travers de contrats sous forme de pré- et post-conditions, ainsi que des clauses reads/writes pour indiquer la portion de la mémoire accédée en lecture/écriture. Dans le but de faciliter la preuve de correction des procédures implémentées, leur corps peut être instrumenté par des invariants de boucles, des variants justifiant la terminaison ou encore par des assertions intermédiaires.
Les obligations de preuve sont générées par l’outil à partir du programme ainsi annoté et spécifié en utilisant un calcul de plus faibles pré-conditions. L’un des atouts de Why3 est que ces obligations de preuve peuvent être envoyées à de nombreux démonstrateurs automatiques ou interactifs. Le système permet également d’appliquer des transformations logiques des obligations de preuve avant de les envoyer aux démonstrateurs.
Par exemple, lorsqu’une obligation de preuve correspond à une conjonction des buts, il est possible de la transformer en une liste de buts qui peuvent alors être pris en charge par des démonstrateurs différents.
WhyML peut également être utilisé pour développer des théories logiques, modélisant divers concepts mathématiques ou informatiques, notamment des structures de données. Pour cela, le langage dispose d’une logique de premier ordre avec des types polymorphes, des définitions de types algébriques, des types abstraits, des prédicats (co-)inductifs et des définitions de fonctions récursives. Des exemples de telles théories peuvent être trouvés dans la bibliothèque standard de Why3. Par exemple, on peut trouver la théorie des entiers, des flottants, ou encore la théorie des ensembles et des séquences. Cette bibliothèque standard, ainsi qu’une présentation bien plus détaillée de Why3, est disponible en ligne sur le site du projet http://why3.lri.fr.

Table des matières

1 Introduction 
1.1 Question de confiance
1.2 Méthodes formelles
1.2.1 Systèmes de types
1.2.2 Vérification déductive des programmes
1.2.3 L’outil de vérification Why3
1.3 Contributions de cette thèse
1.3.1 Code fantôme
1.3.2 Contrôle statique des alias
1.3.3 Raffinement des données
1.4 Plan
Bibliographie
2 Code fantôme 
2.1 GhostML : un petit langage avec du code fantôme
2.1.1 Syntaxe de GhostML
2.1.2 Sémantique opérationnelle de GhostML
2.2 Typage des expressions GhostML
2.2.1 Système de types avec effets de GhostML
2.2.2 Correction du typage
2.2.3 Cohérence des effets statiques avec les effets observables
2.3 Effacement du code fantôme
2.3.1 Opération d’effacement du code fantôme
2.3.2 Correction de l’effacement
2.4 Implémentation
2.4.1 Structure des files mutables avec un champs fantôme
2.5 Travaux connexes
Bibliographie
3 Régions 
3.1 RegML : un petit langage avec des régions
3.1.1 Syntaxe
3.1.2 Sémantique
3.2 Système de types avec effets de RegML
3.2.1 Types
3.2.2 Effets
3.2.3 Typage des fonctions
3.2.4 Règles du typage
3.3 Correction du typage
3.4 Implémentation
3.5 Travaux connexes
Bibliographie
4 Raffinement des données 
4.1 Introduction
4.1.1 Développement modulaire des programmes
4.1.2 Obtention de programmes corrects par construction
4.1.3 Raffinement des types enregistrements
4.1.4 Le problème d’aliasing
4.2 Extension de RegML avec des régions privées
4.3 Raffinement
4.3.1 Raffinement des types
4.3.2 Raffinement des signatures de fonctions
4.3.3 Préservation du typage par le raffinement
4.4 Travaux connexes
Bibliographie
5 Conclusion 
5.1 Choix et limitations
5.2 Perspectives
A Étude de cas : Tables de hachage « Coucou »
A.1 Introduction
A.2 Présentation de l’approche
A.3 Implémentation
A.3.1 Préliminaires : prédicat d’égalité, fonctions de hachage
A.3.2 Définition du type des tables de hachage
A.3.3 Opération de création et test d’appartenance
A.3.4 Ajout d’un élément sans redimensionnement
A.3.5 Changement des fonctions de hachage
A.3.6 Redimensionnement
A.3.7 Ajout d’un élément : cas général
A.3.8 Suppression d’un élément
A.3.9 Preuve
A.4 Typage
Bibliographie

Télécharger le rapport complet