Soutenance mémoire
L’informatique est née de l’étude et de la formalisation du calcul. Dès l’antiquité, des nécessités concrètes ont requis l’étude de longueurs, de surfaces, de volumes, de grandeurs numériques. Les mathématiques émergèrent de la recherche systématique de propriétés sur ces objets. Les démonstrations rigoureuses ont nécessité la définition formelle de concepts comme le rectangle, le cercle, plus tard l’équation, la fonction numérique, etc.
Ces manipulations requerraient des calculs et des raisonnements, lesquels furent donc des outils centraux des mathématiques et des autres sciences, sans être véritablement des objets d’étude systématique et générale à part entière. Au dixneuvième siècle, la recherche des fondements des mathématiques, qui se manifeste entre autres par le développement de la théorie des ensembles de Cantor, la volonté de réduire les mathématiques à la logique de Frege et certains des problèmes de Hilbert, conduisent à des interrogations plus fines sur la nature du raisonnement et du calcul. Naissent alors les controverses entre finitistes de Brouwer et les hilbertiens. D’outils, certes importants, le raisonnement et le calcul deviennent des objets d’étude qui doivent à leur tour être formalisés.
Les différentes approches pour formaliser la notion intuitive de calcul aboutissent dans les années 1930 lorsque Gödel, avec Herbrand, Church et Turing proposent chacun un modèle — fonctions récursives, lambda-calcul, machine de Turing — de cette notion et qu’est démontrée l’équivalence entre ces trois modèles. La thèse de Church postule que ce triple modèle est la bonne formalisation de la notion de calcul, que ce qui est calculable au sens intuitif est ce qui est calculable au sens de ces trois modèles. Car ces études montrent, théorème d’incomplétude de Gödel et indécidabilité du problème de l’arrêt des machines de Turing en tête, que la volonté de Hilbert de réduire le raisonnement mathématique à des étapes de calcul est irréalisable.
Vérification et atteignabilité
Les programmes
Un programme est la description d’un calcul à effectuer par une machine. Il peut être écrit directement dans le langage de la machine ou dans un langage, dit langage de programmation, destiné à être traduit automatiquement dans le langage de la machine au moyen d’un autre programme appelé compilateur. Le langage de programmation doit pouvoir être traité par les opérations calculatoires du compilateur et doit donc proposer une syntaxe formalisée. Pour que le programmeur sache quel programme écrire en vue du comportement qu’il souhaite, le langage de programmation doit aussi proposer une sémantique précise correspondant à sa syntaxe. Il existe plusieurs types de styles syntaxiques. On peut décrire les programmes par des graphes dont les sommets sont des instructions élémentaires et les arcs représentent les passages possibles d’une instruction à l’autre. Cette représentation, quoique non totalement linguistique, est une forme de langage de programmation. Elle est par ailleurs toujours utilisée dans l’analyse des programmes sous le nom de graphe de flot de contrôle. Les langages de programmation impératifs sont très répandus. Ils reposent sur les concepts d’affectation d’une valeur à une variable, de séquence, de test et de boucle. Pour notre part, nous utiliserons des langages de programmation dits fonctionnels. Ces langages connaissent également le test, mais, dans l’acception restrictive que nous faisons nôtre ici, ni la séquence, ni la boucle, ni l’affectation. En revanche, il est permis de définir des fonctions récursives. Le langage dans lequel nous exprimerons nos exemples est un fragment fonctionnel du langage OCaml [Ler+14].
Il existe plusieurs types de sémantiques [Win93], qui décrivent avec plus ou moins de précision le déroulement attendu de l’exécution des programmes. En première approximation, la sémantique dénotationelle [Sch86] d’un programme est la fonction mathématique dont ce programme réalise le calcul.
Correction et vérification
Spécification
Un programme est écrit pour répondre à un problème, exécuter une tâche. Pour pouvoir espérer démontrer formellement que le programme a un comportement conforme à ce qui est attendu, il faut d’abord formaliser cette attente. Tel est l’objet de la spécification. La spécification décrit les paramètres admissibles et le résultat souhaité, en fonction de ces paramètres. Le programme correspondant est censé décrire, en fonction de ces mêmes paramètres, un calcul permettant d’obtenir ce résultat.
Exemple
Une spécification pour l’exemple précédent indique que les valeurs admissibles pour le paramètre l sont des listes non vides d’éléments ordonnés, et que le résultat renvoyé est le plus petit de ces éléments. On peut restreindre la spécification à des listes non vides d’entiers, par exemple.
Étant donné des paramètres effectifs, l’exécution du programme avec ces paramètres est correcte lorsqu’elle fournit le résultat attendu. Le programme est correct lorsque son exécution est correcte pour tous les paramètres admis par la spécification. Parler du résultat issu de l’exécution de l’appel suppose que les étapes de calcul qui s’enchainent dans cet appel s’achèvent à un moment : si le calcul se poursuit indéfiniment, il n’y a pas de résultat. Il est donc également crucial de s’assurer de la terminaison d’un appel. On dit d’un programme qu’il termine sans plus de précision lorsque tous les appels autorisés par la spécification terminent.
Problème de l’arrêt
La tâche de vérifier la terminaison des programmes ne peut être entièrement automatisée. Elle peut l’être si on la restreint à des catégories restreintes de programmes, mais est insoluble dans sa forme générale.
Théorème 4 (Indécidabilité du problème de l’arrêt [Tur36]).
Soit la question : étant donné un programme P et x un paramètre concret pour ce programme, l’exécution de P avec le paramètre x se termine-t-elle après un nombre fini d’étapes ? Il n’existe pas d’algorithme permettant de répondre à cette question.
Il en découle plus généralement la non-existence d’un algorithme général pour déterminer si un programme donné vérifie une propriété donnée [Ric53]. C’est pourquoi les outils de preuve de programme sont utilisés comme suit : si l’outil a réussi à prouver la propriété cherchée, c’est qu’elle est vraie ; si l’outil n’a pas réussi à prouver la propriété, elle peut être fausse comme elle peut être vraie. Ce point de vue est le contraire de celui adopté pour les tests : si le test détecte un problème, c’est qu’il y en a un ; si le test ne détecte rien, il peut ne pas y avoir de problème comme il peut y en avoir un.
Atteignabilité et non-atteignabilité
Nous souhaitons étudier et développer des méthodes qui assurent le bon comportement des programmes, c’est-à-dire des méthodes de preuve. Une telle méthode vise à établir, étant donné un programme — un calcul à effectuer — et une donnée intiale, que les états successifs au cours du calcul resteront confinés au domaine des états admissibles. Ou encore, qu’il n’est pas possible d’atteindre un mauvais état. Il est donc pertinent d’exprimer l’ensemble des états de calcul qui peuvent être atteints par un programme à partir d’un paramètre.
Exemple
Il est impossible d’effectuer minimum :
cette expression est donc, pour ce programme, un « mauvais état », qui ne doit jamais être atteint. Ici, étant donné un état initial, par exemple minimum [4;8;7], on observe que la définition de minimum conduit à se trouver dans des états comportant les termes minimum [8;7] puis minimum [7]. Il résulte de la présence du premier cas dans le match que minimum [7] fournit immédiatement un résultat ; on ne cherche pas à évaluer minimum .
Atteignabilité en réécriture
Les systèmes de réécriture de termes
Nous exposons maintenant le formalisme qui est utilisé dans la suite de ce document. Les notions exposées ici sont classiques, on en trouvera des présentations dans [BN98 ; Ter03]. Ce formalisme met en jeu des termes et des règles de réécriture agissant sur ces termes. Un terme représente donc un état de calcul à effectuer, tandis que les règles de réécriture décrivent les transformations qui peuvent être apportées à cet état pour faire progresser le calcul. Un terme auquel aucune règle de réécriture n’est applicable est appelé une forme normale ; cette notion recoupe celle de valeur. Ainsi, ce sont les règles de réécriture qui donnent leur sens aux termes.
Termes
Les termes sont écrits à l’aide de symboles de fonctions, y compris les constantes, et de variables. Cet alphabet de base est appelé signature. Les variables trouveront leur rôle particulier dans la définition des substitutions.
Définition
Une signature est la donnée, pour chaque entier naturel k jusqu’à un maximum, d’un ensemble fini de symboles, dit ensemble des symboles d’arité k, ainsi que d’un ensemble au plus dénombrable dont les éléments sont appelés variables. Tous ces ensembles sont deux à deux disjoints. L’ensemble des variables est usuellement noté X. L’ensemble des symboles de fonction d’arité k est usuellement noté Σk , et l’ensemble des symboles de fonctions, toutes arités confondues, est noté Σ.
|
Table des matières
1 Introduction
1.1 Contexte
1.2 Contributions
1.3 Plan
2 Vérification et atteignabilité
2.1 Les programmes
2.2 Correction et vérification
2.2.1 Spécification
2.2.2 Problème de l’arrêt
2.3 Atteignabilité et non-atteignabilité
3 Atteignabilité en réécriture
3.1 Les systèmes de réécriture de termes
3.1.1 Termes
3.1.2 Systèmes de réécriture de termes
3.2 Correction et atteignabilité
3.3 Linéarité
4 Résolution du problème d’atteignabilité
4.1 Régularité
4.2 Préservation de la régularité
4.3 Surapproximation : complétion d’automate
4.3.1 Préliminaires
4.3.1.1 Normalisation d’une transition d’automate
4.3.1.2 Réécriture modulo équations
4.3.1.3 Équations et automates : E-cohérence
4.3.2 Procédure de complétion d’automate d’arbre
4.3.2.1 Completion exacte
4.3.2.2 Fusion équationnelle
5 Gérer les stratégies
5.1 Introduction
5.1.1 Stratégies dans les langages de programmation
5.1.2 Stratégie en profondeur
5.2 Complétion d’automate avec stratégie en profondeur
5.2.1 Préliminaires
5.2.1.1 Formes normales et régularité
5.2.1.2 Automates produits
5.2.1.3 Compatibilité
5.2.2 Procédure de complétion innermost
5.2.2.1 Complétion exacte
5.2.2.2 Fusion équationnelle
5.2.3 Preuves de correction et précision
5.2.3.1 Préliminaires
5.2.3.2 Correction
5.2.3.3 Précision
6 Timbuk
6.1 Timbuk3
6.1.1 Représentation des automates
6.1.2 Conversion des TRS en automates
6.2 TimbukSTRAT
6.2.1 Mise en œuvre de la complétion équationnelle
6.2.2 Construction de l’automate IRR(R)
6.2.3 Limites
6.2.4 Comparaison avec la méthode de [CLM15]
7 Vers l’analyse de programmes fonctionnels
7.1 Priorités sur les règles
7.2 Gestion de l’ordre supérieur
7.2.1 Une analyse de flot de contrôle d’ordre supérieur par PMRS
7.2.1.1 Présentation
7.2.1.2 PMRS faible puis raffinement par contre-exemple
7.2.2 Gestion de l’ordre supérieur avec les systèmes de réécriture
7.3 Types built-ins
7.4 Lien avec l’interprétation abstraite
7.4.1 Présentation informelle de l’interprétation abstraite
7.4.2 Cadre formel confortable
7.4.2.1 Univers et connexions de Galois
7.4.2.2 Opérateurs et leurs abstractions
7.4.3 Perspectives
8 Conclusion
