Ensemble de termes accessibles en réécriture

Résumé

Avant d’exploiter ou de diffuser un logiciel, il convient de s’assurer de sa correction. Lorsque la taille du programme est grande, l’automatisation de la preuve est à rechercher, mais elle ne peut être une panacée (théorème de Rice). Ce rapport s’inscrit dans une étude utilisant les systèmes de réécriture (TRS) comme modèles formels des programmes : la correction s’exprime par le fait que l’ensemble des termes accessibles par le TRS considéré (R(L)) est disjoint d’un ensemble de termes représentant les mauvais comportements (Lm). On sait décider une telle propriété si les langages en jeu sont réguliers (au sens des automates d’arbres). Certaines classes de TRS préservant la régularité sont connues, mais ne couvrent pas tous les cas. Ici, nous nous intéressons à la complétion d’automate : ce procédé vise une sur-approximation régulière de R(L), disjointe de Lm, en ajoutant des transitions à l’automate jusqu’à obtention d’un point fixe. La complétion équationnelle permet de paramétrer la sur-approximation par un ensemble E d’équations entre termes afin de favoriser l’obtention d’un point fixe. Nous exposons cette méthode et tentons de l’exprimer dans le vocabulaire de l’interprétation abstraite, une autre méthode d’élaboration d’analyses statiques.

Introduction

Il est important de s’assurer de la correction des logiciels que l’on écrit, en particulier lorsqu’on envisage de les diffuser. Pour des programmes courts, il est possible d’effectuer une preuve de correction à la main, mais dès que le programme à étudier est long, établir une telle preuve devient très fastidieux.
Les méthodes de vérification ont pour objet d’automatiser l’assurance de correction des programmes.
Il en existe de fort nombreuses, qu’on peut répartir en deux grandes classes. Les méthodes de vérification dynamique sont actives au moment de l’exécution ; il peut s’agir par exemple d’instructions de test qui auront été rajoutées au programme initial. Ces méthodes ne sont pas étudiées ici.
La présente étude s’inscrit dans le cadre de la vérification statique. Le programme est analysé sans qu’il soit exécuté. On souhaite assurer la sureté du programme, c’est-à-dire vérifier qu’aucune de ses exécutions possibles n’atteint un état incorrect. Bien entendu, le théorème de Rice interdit d’espérer obtenir une preuve de correction dans tous les cas : on admet qu’une analyse statique réponde que l’absence d’erreur n’est pas garantie sans qu’elle assure la présence d’une erreur.
Une analyse statique utilise un modèle formel du programme étudié. Ce modèle doit être correct, suffisamment grossier pour que l’analyse termine à coup sûr mais suffisamment précis pour que le résultat de l’analyse soit intéressant.
Les modèles formels utilisés par la complétion équationnelle, qui est l’objet principal de notre étude, sont basés sur les termes et la réécriture. Les termes représentent les états de la machine.
L’exécution d’une instruction correspond alors à la réécriture du terme représentant l’état courant en le terme représentant l’état suivant. L’exemple suivant vise à représenter la fonction factorielle comme un système de réécriture.
Il existe d’autres cadres théoriques permettant de concevoir des analyses statiques. L’un d’eux est l’interprétation abstraite. Il consiste à exécuter le programme dans une sémantique suffisamment grossière pour que le problème de l’arrêt soit contourné.
Au cours de ce stage effectué sous la direction de Thomas Genet au sein de l’équipe Celtique commune à l’IRISA et à l’INRIA Rennes, nous avons tenté d’acquérir une compréhension de la complétion équationnelle et de l’exprimer dans le vocabulaire de l’interprétation abstraite. Ce stage fait suite à notre étude bibliographique [Sal11], 1 et certaines parties du présent rapport (la présente introduction, les sections 2 et 3 ainsi que quelques phrases) en sont issues, après augmentations, remaniements, adaptations ou corrections. 2
Afin que notre tentative de traduction de la complétion équationnelle en le vocabulaire de l’interprétation abstraite soit lisible par les connaisseurs de chacun des deux domaines, il fallait prendre le temps de définir chacun d’entre eux.
C’est pourquoi nous commençons par définir un cadre théorique comprenant les langages d’arbres, les automates d’arbres et les systèmes de réécriture (section 2). Cette section est classique pour celui qui connait ce domaine. Toutefois, des notations non standard mais adaptées à notre étude sont présentées en section 2.2.2. On pourra également lire la remarque 4 et la définition d’un « remplacement ».
Ce cadre nous permet d’énoncer le problème de l’atteignabilité et de mentionner rapidement celui de la préservation de la régularité (section 3).
La section 4 présente la complétion équationnelle d’une manière que nous souhaitons accessible. Nous comptons cette présentation d’une notion ardue au nombre de nos contributions. La section 5 est une présentation résumée mais classique de l’interprétation abstraite. Le connaisseur de ces notions peut ignorer cette section. Nos principales contributions sont présentées en section 6 : une tentative de traduction de la complétion équationnelle en interprétation abstraite.

Automates d’arbres

Nous verrons en section 3 que le problème de vérification que nous étudions se traduit en un problème d’intersection de langages de termes. Ce problème n’est pas décidable en général, mais il l’est si l’on se restreint à des langages d’arbres réguliers.
Cette section s’appuie largement sur [Com+08], mais nous introduisons des notations adaptées à notre étude. Nous ne considérons que des termes clos sur une signature donnée, que nous identifions aux arbres qui les représentent.

Présentation informelle

Réécriture

Termes et arbres

Cette section s’appuie sur [Com+08] et [BN98].
La première étude des termes et leur représentation sous forme d’arbre semble être due à Axel Thue dans [Thu10]. Il énonce qu’en certaines circonstances, on peut, à partir d’un concept A et d’un concept B et en utilisant une opération (binaire) , construire de manière univoque un nouveau concept C, qu’il propose de noter

Automates d’arbres

Présentation informelle

Les automates d’arbres sont l’analogue des automates de mots, souvent appelé « automates » sans plus de précision. Ainsi, les langages réguliers dont il est question dans ce rapport sont les langages d’arbres reconnus par des automates d’arbres.
Nous supposons que le lecteur est familier de la notion d’automate de mots, et nous présentons les automates d’arbres par analogie. Commençons par dire qu’on n’aura pas, comme c’est le cas pour les automates de mots, de représentation agréable de l’automate sous la forme d’un graphe. Mais voyons une façon d’appréhender le fonctionnement d’un automate de mots :
Généralisons ce comportement aux arbres. Contrairement à un mot, un arbre n’a pas un début et une fin, mais une racine et des feuilles (étiquetées par des symboles de constantes). Les automates que nous considérerons ici « commencent » à agir sur les feuilles. Contrairement au cas des mots, où n’importe quelle lettre peut être le début d’un mot à traiter, les premières étapes de l’exécution d’un automate d’arbre ont nécessairement lieu sur des symboles de constantes. On n’a donc pas besoin de notion d’état initial : il suffit d’avoir des transitions initiales qui s’appliquent aux symboles de constantes.
Exemple 18.
Construisons un automate d’arbre qui reconnait le langage

Définitions

Considérons la représentation unaire des entiers naturels munie de l’addition. Nous savons déduire des axiomes de neutralité additive de zéro (x + 0 = x) et de compatibilité de l’addition avec le successeur désignent le même entier. Pour avoir un espoir d’obtenir un tel résultat automatiquement, il faut indiquer à l’ordinateur que l’égalité de chacun des deux axiomes est utilisée dans le sens de gauche à droite.
Voilà ce qu’est une règle de réécriture : une égalité orientée.

Définition 35 (Règle de réécriture)

Une règle de réécriture sur est un couple de termes qu’on note. On impose, pour cette notion, que ne soit pas une variable et que toute variable présente dans r soit également présente dans.
Définition 36 (Système de réécriture de termes).
On appelle système de réécriture (de termes) sur tout ensemble de règles de réécriture sur ce langage.

Théories équationnelles

Certaines égalités ne peuvent pas être orientées pour définir des règles de réécriture, comme par exemple les égalités traduisant la commutativité d’un opérateur binaire : il n’y a pas de sens à privilégier, et donner les deux orientations conduit à un système de réécriture qui « boucle » en passant d’une forme à l’autre. La réécriture modulo équations a été introduite pour résoudre ce problème : on renonce à orienter les égalités en cause, mais l’on considère équivalents des termes qui sont en relation par ces égalités, et l’on réécrit les classes d’équivalence.
Mais ce n’est pas pour résoudre ce problème que nous introduirons des équations : nous nous en servirons pour paramétrer la sur-approximation de la complétion équationnelle. Nous allons définir des relations d’équivalence, mais il faut qu’elles soient « compatibles avec l’application des fonctions », c’est-à-dire que ce soient des congruences.
Le point délicat est bien sûr la boucle : nous ne savons pas si elle va être empruntée, ni combien de fois. Nous devons donc envisager plusieurs cas possibles.
Supposons que la boucle est empruntée une première fois : à la ligne 7, l’expression a + 2 vaut P, et donc l’affectation donne à a la valeur P (qu’elle avait déjà) ; à la ligne 8, l’expression b + 1 vaut I (car b vaut P depuis la ligne 4), et l’affectation courante donne donc à b la valeur I.
Considérons maintenant un passage quelconque dans la boucle. Par propagation, nous pouvons affirmer que la valeur de a est toujours P (elle n’est pas modifiée par le passage dans le boucle). En revanche, selon que nous sommes, par exemple, dans le premier ou dans le deuxième passage de la boucle, nous ne savons pas si b contient la valeur P ou la valeur I. Nous n’avons pas d’autre choix que de considérer cette valeur comme inconnue : >.
Mais qu’importe : au début de la ligne 10, nous ne savons pas si la boucle a été exécutée ni combien de fois, donc nous n’avons pour b pas de valeur plus précise que >. En revanche, nous avons vu que quelque soit la situation, a contient la valeur P. C’est précisément ce que nous voulions vérifier.
Notons que si la ligne 5 du programme avait été ainsi rédigée : a = d + d;, notre analyse aurait échoué, car elle n’aurait pas pu déterminer que cette instruction affecte nécessairement une valeur paire à a. En effet, à la ligne 5, d contient la valeur abstraite >, si bien que la sémantique abstraite de + donne le résultat >.

Cadre formel confortable

Univers et connexions de Galois

Les valeurs abstraites envisagées pour une analyse sont appelées propriétés abstraites, leur ensemble forme l’univers abstrait. De même que dans la section précédente, nous considérions > comme moins précis que P, nous avons besoin d’une relation d’ordre sur l’univers abstrait pour dénoter la précision relative des propriétés abstraites. Étant donné deux propriétés p et q, nous souhaitons que l’univers abstrait possède une propriété qui puisse tenir le rôle de « p ou q ». Cette propriété doit être moins précise que p (au-dessus de p, pour notre relation d’ordre), moins précise que q (au-dessus de q), mais plus précise que toute autre propriété qui est à la fois au-dessus de p et de q.
Finalement, il est souhaitable que toute paire de propriétés fp;qg possède une borne supérieure pour la relation d’ordre. De même, il faut qu’elle possède une borne inférieure, qui joue le rôle de « p et q ». Ces considérations nous conduisent à imposer que l’univers abstrait soit un treillis.

Conclusion

L’objectif du stage était d’acquérir une compréhension de la complétion équationnelle, de l’exposer d’une manière accessible (section 4) et de tenter d’étendre son efficacité. Au cours du stage, il est apparu souhaitable d’essayer d’exprimer la complétion équationnelle dans le vocabulaire de l’interprétation abstraite (section 6).
L’étude menée conduit à un résultat négatif. La première étude (section 6.2) a donné une condition nécessaire de déterminisme et d’universalité contraignante, si bien que nous ne voyons pas dans l’immédiat d’abstraction correcte pertinente de R. La deuxième étude (section 6.3), qui abandonne le cadre confortable des connexions de Galois, fournit une réponse triviale : l’identité est une abstraction correcte de R et de R.
Toutefois, des pistes peuvent être explorées d’ici la fin du stage ou à plus lointaine échéance.
L’opérateur abstrait de la première étude semble pouvoir être rapproché de la « réécriture à la racine » de [Boy10]. De plus, d’autres domaines abstraits peuvent éventuellement être envisagés. Par ailleurs, l’étude des tautologies (section 6.1) a permis d’entrevoir, comme dit en remarque, une analogie avec des procédés d’apprentissage automatique. Des stratégies d’apprentissage avec exemples et contre-exemples seraient à étudier, le rôle des exemples étant tenu par L0 et celui des contre exemples par Lbad. Thues Arbeit ist ein Musterbeispiel dafür, wie weit die Zitationsrate und die bahnbrechende Originalität eines wissenschaftlichen Artikels auseinanderklaffen können. [. . . ] Und so fällt sie nach allen gängigen Maßstäben der Bibliometrie in die Kategorie „bedeutungslos“. Die Historie gibt dieser Einschätzung in gewissem Sinne auch recht, denn die Theorie der Termersetzung hat sich ja unabhängig von Thues Arbeit entwickelt. Dennoch wird jeder, der wissenschaftliche Originalität und Substanz zu schätzen weiß, Thues Arbeit von 1910 zu den besten Juwelen der Wissenschaft zählen.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela chatpfe.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières
1 Introduction
1.1 Notations générales
2 Réécriture
2.1 Termes et arbres
2.1.1 Généralités
2.1.2 Propriétés des termes, Contextes
2.2 Automates d’arbres
2.2.1 Présentation informelle
2.2.2 Définitions et intérêt
2.3 Systèmes de réécriture
2.3.1 Définitions
2.3.2 Propriétés des systèmes de réécriture
2.3.3 Théories équationnelles .
3 Le problème de l’atteignabilité
4 Complétion équationnelle
4.1 Introduction
4.2 Présentation informelle
4.3 Définition et première étude
4.3.1 Complétion exacte
4.3.2 Simplification équationnelle
4.3.3 Complétion équationnelle
4.3.4 R=E-cohérence
4.4 Correction et précision
5 Interprétation abstraite
5.1 Présentation informelle
5.2 Cadre formel confortable
5.2.1 Univers et connexions de Galois
5.2.2 Opérateurs et leurs abstractions
6 Complétion en interprétation abstraite
6.1 Préliminaires
6.2 Première étude
6.2.1 Univers et connexion
6.2.2 Opérateur abstrait : difficulté
6.2.3 Nécessité des hypothèses
6.3 Deuxième étude
7 Conclusion