TP de traitement des formules propositionnelles
Contents
1. L algorithme de mise en NNF est en fait s par en deux parties La premi re partie se concentre sur l limination des constantes Celle ci est faite par les m thodes virtuelles suivantes de la classe Nnf abstract public Nnf and Nnf right quivalent this amp right abstract public Nnf or Nnf right quivalent this right Attention contrairement ce qui se passe dans la classe Prop ces m thodes ne correspondent pas directement aux constructeurs And et Or de la signature Nnf Dans la deuxi me partie on peut donc se concentrer sur la propagation de la n gation vers les feuilles en comptant sur les m thodes de la premi re partie pour liminer les constantes Concr tement la deuxi me partie consiste impl menter la m thode virtuelle suivante de la classe Prop abstract public Nnf toNnf boolean neg de telle fa on que x toNnfO puisse tre impl ment e par x toNnf false et telle que x toNnf true retourne une Nnf logiquement quivalente x negO toNnf 0 Le r le du bool en neg est de m moriser si on doit propager une n gation vers les feuilles ou pas sachant qu une double n gation quivaut aucune n gation De plus lorsque la propagation d une n gation traverse le n ud un And ou un Or on utilise les lois de De Morgan voir http en wikipedia org wiki De_Morgan s_laws un And se transforme en Or et r ciproquement Pour le n ud Implies il suffit2. d utiliser l quivalence logique Implies X Y quivaut Or Neg X Y pour se ramener aux cas pr c dents Pour tester votre m thode toNnf utilisez les classes internes de Test pr fix es par Nnf sur les diff rents cas de test 5 T che 4 tests sur la r solution de grilles de sudoku Lorque votre m thode de mise en NNF semble bien fonctionner testez l sur un vrai exemple la r solution des grilles de sudoku Pour cela on va utiliser un SAT solver appel clasp tant donn une formule propositionnelle dans une certaine forme qu on va pr ciser plus loin ce logiciel r pond soit UNSATISFIABLE aucun environnement ne satisfait la formule soit SATISFIABLE et dans ce cas affiche un environnement qui satisfait la formule Ce logiciel impl mente une variante de l algorithme DPLL qui vous sera ventuellement pr sent dans le cours de logique voir avec l ensei gnant concern La formule en entr e de cet algorithme doit tre en CNF pour Conjunctive Normal Form ou forme normale conjonctive en fran ais Une telle formule est une NNF dans laquelle toute sous formule ou sous arbre d un n ud Or ne contient pas de n ud And La NNF de l exemple introductif 1 2 est bien une CNF Par contre une formule comme 1 amp 2 3 est une NNF qui n est pas une CNF Na vement pour mettre une formule NNF en CNF il suffit d appliquer la distributivit du Or sur le And une for
3. de eclipse 8 2 Br ve description des classes Java fournies voir fichiers de src La classe Erreur d clare l unique exception directement lev e par les sources fournies en dehors de Lexer et PrefixParser La classe Prop A COMPLETER sections 2 et 4 d finit la structure d AST des formules propositionnelles La classe Environment d finit les environnements et les entr es sorties sur les environnements La classe Test fournit quelques tests simples sur les manipulations d AST La classe Nnf A COMPLETER sections 3 et 4 d finit une structure d AST pour repr senter des formules sous forme NNF La classe Sudoku fournit les tests partir des grilles de Sudoku La classe PrefixParser A COMPLETER section 6 fournit le squelette d analyseur syntaxique en notation pr fixe La classe Token fournit la structure de lex mes abstraits utilis e par l analyseur syntaxique La classe Lexer A CORRIGER section 6 fournit l analyseur lexical utilis par les analyseurs syntaxiques La classe InfixParser A COMPLETER section 7 fournit le squelette d analyseur syntaxique en notation infixe 2014 2015 page 14 14
4. de sorte que le d veloppeur peut directement crire son parser dans un format proche de celui de la sp cification donn e en 7 1 Mais le but de ce TP est justement de faire ces transformations la main sur un petit exemple afin d acqu rir la compr hension du fonctionnement de ces outils qui s av re indispensable quand on les utilise sur des exemples plus complexes 7 1 Sp cification de la syntaxe infixe La sp cification du parser infixe est donn e par la BNF attribu e ci dessous et les r gles de pr c dence donn es plus loin Cette BNF comporte un seul non terminal et axiome not P Ses terminaux sont pos et tous les symboles entre apostrophes Le syst me d attribut sp cifie les AST associ s aux mots reconnus par le parser Les profils des symboles de la BNF sont donn s par PfProp posfPos La BNF attribu e est Po z 7t p True f p False posfv p Var v 7 P pi p Neg p CE PI Pfp1 amp Pfp2 p And p1 p2 Pfp1 l Pi p Or p1 p2 Pfp1 gt Pin p Implies p1 p2 Cette BNF ci dessus est ambigu pour un m me mot plusieurs AST peuvent tre synth tis s Pour d sambigu ser on restreint les arbres d analyses possibles en utilisant les r gles de pr c dences ci dessous les op rateurs ont les niveaux de pr c dence suivants op rateur pr c dence 2 gt 2 3 2 2 2 2 amp 2 1 i 9 0 comme dans tout langage d expression les cons
5. de type Nonconstant Cast o est repr sent par le cast Java Nnf o on peut en fait laisser ce cast implicite en g n ral 3 2 faire La traduction des AST de sorte Nnf en sorte Prop est d clar e dans la classe Nnf par la m thode virtuelle abstract public Prop toProp Vous devez modifier le fichier Nnf java fourni de mani re impl menter la m thode toProp qui retraduit une formule Nnf en formule Prop Testez votre impl mentation sur le cas de test mpx du fichier Test java 4 T che 3 mise en forme normale n gative La t che 3 consiste impl menter l algorithme qui permet de traduire n importe quelle formule de type Prop en une formule de type Nnf qui soit logiquement quivalente Concr tement cette traduction est effectu e dans la m thode suivante de la classe Prop public Nnf toNnf Ainsi pour tout x de type Prop et tout env de type Environment on veut x eval env x toNnf toProp eval env Par ailleurs pour y de type Nnf l arbre y toPropO toNnf doit tre identique l arbre y 8 traduit par literal en anglais 2014 2015 page 7 14 Ensimag 1A App TP intro aux traitements des langages On attend aussi que le co t de votre algorithme toNnf soit lin aire en fonction du nombre de n uds travers s et m me on attend un seul parcours de l arbre De m me la taille de l arbre produit en nombre de n uds doit aussi tre lin aire
6. sent s comme des m thodes virtuelles dont le premier argument est implicitement l objet auquel elle s applique Ainsi la formule de l exemple introductif est cod e comme un objet de type Prop construit par Prop TRUE and Prop var 1 implies Prop var 2 neg On aurait videmment pu choisir un codage diff rent en n utilisant par exemple que des m thodes statiques et pas de m thode virtuelle Attention ici ne pas confondre le mot constructeur d une signature employ dans le contexte des signatures multisort es et la notion de constructeur Java Bien que les deux notions soient reli es voir section 1 3 il ne faut pas les identifier Le principal int r t d une telle structure d AST est de permettre la programmation des traitements 2 En cours on l crira plut t sans parenth se mplies And True Var 1 Neg Var 2 En effet avec les constructeurs crits avant leurs arguments il n y a qu une fa on de parenth ser qui respecte le typage des constructeurs 2014 2015 page 2 14 Ensimag 1A App TP intro aux traitements des langages sur le langage ind pendamment de l analyse syntaxique on d taille une fa on de programmer ces traitements en section 1 3 Le deuxi me int r t de cette structure est qu elle facilite l criture d un programme Java qui g n re une formule de type Prop En effet le compilateur Java v rifie statiquement que les formules g n r
7. 2015 page 3 14 Ensimag 1A App TP intro aux traitements des langages dont le constructeur Java a une liste d arguments correspondant S1 x x Sn qui permet d initialiser la liste d attributs Voir le code esquiss ci dessous correspondant respectivement aux constructeurs And et Var class And extends Prop class Var extends Prop final Prop left right final int value And Prop left Prop right Var int value this left left assert value gt O this right right this value value Dans le fichier fourni Prop java les sous classes de Prop sont priv es et statiques alternative ment on aurait pu utiliser un m canisme de paquetage pour r aliser cette encapsulation Au niveau de la classe Prop les m thodes and et var sont simplement des appels ces constructeurs Java public Prop and Prop right static public Prop var int value return new And this right return new Var value Dans chacune de ces sous classes les m thodes virtuelles d clar es au niveau de Prop peuvent ainsi tre impl ment es en fonction du n ud repr sent Typiquement on illustre ce principe sur l exemple de la m thode abstract void printPrefix O d clar e au niveau de la classe Prop qui permet d afficher l AST sous forme textuelle en notation pr fixe Le principe de cet affichage est le suivant en chaque n ud on affiche d abord l op rate
8. Ensimag 1A A TP intro aux traitements des langages 8 pp gag TP de traitement des formules propositionnelles Ce TP introduit les concepts du cours de traitements des langages informatiques dans le cas particulier du langage des formules propositionnelles Ce TP sert donc aussi d introduction au cours de logique qui sert ici d application du cours de TL Les formules propositionnelles sont des expressions qui ne contiennent que des op rations et des va riables propositionnelles Concr tement une telle formule est ici constitu e partir des constantes t vrai et f faux des variables bool ennes nomm es en utilisant des entiers strictement positifs de la n gation logique ainsi t vaut f et des op rateurs binaires suivants amp et logique ou logique gt implication logique Par exemple t amp 1 gt 2 se lit vrai et 1 impliquent non 2 Ce langage est donc un des plus simples qu on puisse imaginer Ceci dit il est suffisamment expressif pour exprimer des probl mes comme celui du sudoku qui va nous servir de cas de test significatif cf section 5 On appelle analyseur syntaxique ou parser en anglais un programme informatique capable de lire une suite de caract res comme t amp 1 gt 2 et de l interpr ter comme une formule logique crire un tel programme est un probl me priori non trivial mais qui a des solutions bien comp
9. Ici la m thode oracle v simule le r sultat attendu de exintro test eval v partir de l pour chaque traitement tester et chaque cas de test la classe Test d finit un pilote au moyen d une classe interne avec sa propre m thode main Le nom du cas de test appara t en suffixe dans le nom de la classe interne Par exemple pour tester l affichage pr fixe sur exintro on lance java ea Test Printexintro Pour tester la m thode eval il faut utiliser les classes internes pr fix es par Eval Le main associ attends alors un liste de noms de variables strictement positifs en arguments de la ligne de commande Il value alors le cas de test avec l environnement qui associe t une variable si et seulement si celle ci figure dans la liste en argument 6 La terminologie utilis e ici correspond s emploie fr quemment pour les langages d expression comme les expressions arithm tiques En logique on utilise interpr tation ou mod le la place de environnement Et l valuation correspond la relation de satisfaisabilit un mod le satisfait une formule revient donc au fait que l valuation de cette formule sur ce mod le r pond vrai 7 lancer apr s avoir compil et positionn le CLASSPATH comme expliqu en section 8 2014 2015 page 5 14 Ensimag 1A App TP intro aux traitements des langages Ainsi la commande java ea Test Evalexintro 1 2 doit afficher eval false Et
10. ST de sorte Prop ce qui permet donc d appliquer ensuite les traitements impl ment s au niveau de la classe Prop comme printPrefix ou eval 2014 2015 page 6 14 Ensimag 1A App TP intro aux traitements des langages 3 1 D finition des AST de sorte Nnf Tout d abord on appelle litt ral une formule qui est soit r duite un nom de variable soit la n gation d un nom de variable Ici un tel litt ral est directement cod par un entier non nul On introduit donc la sorte externe NNInt comme ensemble des entiers non nuls On introduit aussi les sortes internes Nonconstant pour d signer les NNF non constantes et Nnf pour d signer les NNF quelconques On exprime ainsi directement les contraintes syntaxiques de la forme NNF par des r gles de typage True Nnf False Nnf Cast Nonconstant Nnf And Nonconstant x Nonconstant Nonconstant Or Nonconstant x Nonconstant Nonconstant Literal NNInt Nonconstant La signification des constructeurs se d duit directement de leur nom En particulier une formule Cast X repr sente exactement la m me formule que X L impl mentation de cet AST dans la classe Nnf suit la d marche d crite en section 1 3 ceci pr s que le constructeur Cast n est pas repr sent comme une classe du fait de sa signification tr s particuli re En Java on peut simplement le repr senter en faisant de la classe abstraite Nonconstant une sous classe de Nnf tant donn un objet o
11. btenue est non ambigu Cela va tre v rifi de mani re indirecte en la transformant en BNF LL 1 7 3 A faire transformer la BNF non ambigu en une BNF LL 1 Vous devez maintenant transformer la BNF de la section 7 2 en BNF LL 1 vous devez obtenir une BNF attribu e LL 1 qui reconna t le m me langage et synth tise les m mes AST que celle de la section 7 2 Comme il n y a que des op rateurs associatifs droite il suffit en principe de factoriser les r gles gauche En cas d op rateurs associatifs gauche il faudrait liminer les r cursions imm diates gauche V rifiez que la BNF est bien LL 1 en effectuant le calcul de directeurs 7 4 A faire impl menter le parser LL 1 Votre travail consiste maintenant impl menter le parser sp cifi section 7 1 en le d rivant de la BNF LL 1 obtenue en section 7 3 Concr tement il s agit de compl ter le fichier fourni InfixParser java en modifiant la m thode parseProp de mani re ce qu elle accepte tout pr fixe de l entr e qui est un sous mot de P3 et produise l AST associ Comme vu en CTD il faut ventuellement introduire une m thode sp cifique pour chaque autre non terminal de la BNF LL 1 Pour tester que le parser fonctionne commencez par utiliser le jeu de tests du sous r pertoire infix partir du script testinfix sh Une fois que tous ces tests fonctionnent correctement essayez un test plus cons quent avec testparser_sudok
12. e ceux commen ant par ko_ 12 http www satcompetition org 2009 format benchmarks2009 html 2014 2015 page 9 14 Ensimag 1A App TP intro aux traitements des langages doivent tre rejet s ils contiennent des erreurs de syntaxe Par exemple le fichier ok_exparser prop contient 4 exemple de formule en notation pr fixe amp 421 f Il est constitu de 4 lex mes amp 421 et f Et PAST correspondant est cette formule est And Var 421 Neg False Pour simplifier la programmation de l analyseur syntaxique celui ci est d compos en deux parties l analyseur lexical ou lerer en anglais qui transforme la suite de caract res en suite de lex mes cf section 6 1 et l analyse syntaxique proprement dite qui construit AST partir de la suite de lex mes cf section 6 2 6 1 Analyse lexicale On fournit ici l analyseur lexical dans le fichier Lexer java Typiquement la commande suivante permet d afficher sur une ligne part chaque lex me d un fichier donn NB le fichier est lu sur lentr e standard java ea Lexer lt prefix ok_exparser prop En interne pour chaque lex me concret c est dire une certaine suite de caract res reconnu lana lyseur construit un lex me abstrait c est dire un objet Java du type fourni Token Ainsi l analyseur lexical est en fait un objet de type Lexer qui fonctionne comme une sorte d it rateur Java il a essen tiellement une m th
13. ent de la fa on de les repr senter dans tel ou tel langage de programmation Cette notation sera formellement d finie en cours On se contente ici de la pr senter de mani re intuitive 1 Historiquement beaucoup des concepts de TL sont d ailleurs issus de la formalisation de la logique 2014 2015 page 1 14 Ensimag 1A A TP intro aux traitements des langages 8 pp gag 1 1 Une notation pour les structures d AST Dans le cours on formalise une structure d AST comme une signature multisort e repr sentable dont le r le est de d finir la forme possible des arbres Une telle signature est donn e par un ensemble fini de sortes qui nomment des types d arbre un ensemble fini de constructeurs qui correspondent des noms crits sur les n uds et un type ou profil pour chaque constructeur Ce type per met de consid rer le constructeur comme une fonction qui tant donn un n uplet d arbres avec ventuellement n 0 retourne un nouvel arbre dont ceux l sont les fils Concr tement ce type donne la sorte attendue de chaque fils du constructeur ainsi que la sorte des arbres dont le construc teur est racine Dans le cas des formules propositionnelles on uti True Prop lise deux sortes Prop pour le type des formules False Prop et Pos pour le type des entiers strictement positifs Neg Prop Prop qui repr sentent des noms de variables On intro And Prop x Prop Prop duit ensuite un constructeur pour cha
14. es sont bien form es pour toute ex cution du programme Java Par exemple on ne peut pas crire de programme Java compilable qui g n rerait une formule mal form e correspondant amp 1 L analyseur syntaxique va tre lui m me un exemple d un tel programme 1 2 Exemple du sudoku Un autre exemple de programme qui g n re une formule Prop est donn par la m thode initSudokuRule du fichier fourni Sudoku java tant donn un entier n valant typiquement 4 ou 9 cette m thode calcule une formule qui exprime la r gle du jeu du sudoku n cases disponible en fran ais sur http www e sudoku fr regle grille sudoku php 3 variables propositionnelles chacune des n cases Ici l tat d une grille de sudoku est cod par n de la grille on associe n variables telles que pour p 1 n la p i me variable de la case vaut vrai ssi l entier p est crit sur la case C est la m thode var dans ce m me fichier qui exprime ce codage des noms de variable x Nom de variable associ un choix de nombre sur une case param i num ro de ligne requiert O0 lt i lt n param j num ro de colonne requiert 0 lt j lt n param p nombre crit sur la case requiert 1 lt p lt n return nom de variable correspondant au choix de poser p en case i j public static Prop var int p int i int j return Prop var i xn j xn p J La formule retourn e par initSudokuR
15. es lex mes parmis amp gt Pour chaque fils attendu on effectue en s quence un appel r cursif recParse afin de r cup rer AST correspondant Si l exception Lexer ErreurSyntaxe est lev e dans un des appels r cursifs c est que le v n existe pas on laisse l exception se propager Dans le cas contraire on retourne l AST obtenu par assemblage du n ud initial et de ses fils La m thode principale de l analyseur syntaxique se contente d appeler recParse et de v rifier qu en sortie de l appel on a bien atteint la fin du fichier Prop mainParse 6 3 faire Votre travail consiste compl ter la m thode recParse d crite ci dessus fournie dans le fichier PrefixParser java La m thode Lexer nextVar fournie contient des bogues que vous devez cor riger apr s avoir compris ce qu elle est cens e faire 15 Pour tester que le parser fonctionne on commencera par utiliser le jeu de tests du sous r pertoire prefix sur l ex cutable java ea PrefixParser prefix Celui ci commence par l analyse syn taxique de l entr e standard Si celle ci choue alors un message d erreur est affich Sinon PAST construit est r affich en syntaxe pr fixe Au cours des tests v rifiez que les fichiers pr fix s par ko_ provoque le message d erreur indiqu en commentaire en d but du fichier les fichiers pr fix s par ok_ sont r affich s sans erreur Une fois
16. ge 10 14 Ensimag 1A App TP intro aux traitements des langages lecture du fichier s interrompt la premi re erreur detect e dans le fichier Pour programmer l analyseur syntaxique on se base sur la propri t suivante de la notation pr fixe Pour toute suite de lex mes u il existe au plus une suite de lex mes v qui est un pr fixe de u et qui correspond l criture en notation pr fixe d un AST de sorte Prop Par exemple si u correspond amp t 1 2 alors l unique v possible correspond amp t 1 Par contre si u correspond amp t il n y a aucun v possible Cette propri t permet en effet de programmer r cursivement une m thode recParse qui tant donn la suite u des lex mes restant lire s il existe un pr fixe v de u tel que v est l criture en notation pr fixe d un AST de type Prop alors recParse retourne cet AST et la t te de lecture du lexer apr s l appel se trouve sur le premier lex me apr s la suite v dans u 14 si un tel v n existe pas alors recParse l ve l exception Lexer ErreurSyntaxe Prop recParse L unicit du v recherch permet en effet une programmation r cursive simple de cette proc dure le premier lex me de v et donc u n est pas la sentinelle de fin sinon on l ve l exception et correspond un n ud dont on conna t le nombre de fils 0 pour t ou f ou un nom de variable 1 pour et 2 pour l
17. la com mande java ea Test Evalexintro 1 doit afficher eval true Si l valuation du cas de test diff re de sa m thode oracle une erreur sera lev e l ex cution Vous devez tester ainsi votre m thode eval sur les diff rents cas de tests et sur diff rentes valeurs de l environnement Vous pouvez aussi ajouter d autres cas de tests notamment pour faciliter le d bogage 2 2 Tests des grilles de sudoku Une fois que vous pensez que votre m thode eval fonctionne bien vous pouvez l utiliser sur un exemple plus significatif la v rification qu une grille de sudoku respecte les r gles donn es par initSudokuRule 3 Pour commencer on se limite aux grilles de sudoku de taille 4 dans le fichier Sudoku java fourni la constante n est fix e 4 dans les fichiers sudoku4 Syntaxiquement ces fichiers sont construits en partant du fichier sudoku4 vide et en rempla ant certains caract res _ repr sentant une case vide de la grille par un chiffre entre 1 et n Une m thode statique de la classe Sudoku appel e PuzzleReader read permet de construire l environnement repr sentant une telle grille PuzzlePrinter print permet de r afficher un tel environnement sous forme de grille Pour tester une grille il suffit d ex cuter la m thode main de la classe Sudoku Checker en passant la grille sur l entr e standard java ea Sudoku Checker lt sudoku4 2169 V rifiez que toutes les g
18. le bool en obtenu lorsqu on remplace dans X chaque nom de variable par sa valeur dans l environnement et qu on calcule l expression bool enne sans variable ainsi obtenue Sur l exemple introductif t amp 1 gt 2 si l environnement associe t aux variables 1 et 2 alors la formule s value sur le bool en t amp t gt t qui vaut t gt f c est dire f Si l environnement associe t 1 et f 2 alors la formule s value sur t amp t gt f qui vaut t gt t c est dire t Concr tement l environnement env en param tre de eval est un objet de type Environment qui a une m thode get associant chaque un bool en chaque nom de variable public class Environment public boolean get int name requiert name gt 0 2 1 Tests de base Pour d boguer votre m thode eval il faut la tester partir des programmes fournis dans le fi chier Test java La classe Test contient des attributs statiques d finissant des cas des tests de type TestCase Typiquement l exemple introductif du sujet est d fini par public final static TestCase exintro new TestExIntro avec class TestExIntro extends TestCase TestExIntro initialise attribut public Prop test super Prop TRUE and Prop var 1 implies Prop var 2 neg boolean oracle Environment v return implies true amp amp v get 1 v get 2
19. mule Or And X Y Z est traduite en la formule quivalente And Or X Z Or Y Z Mais cet algorithme augmente la taille de la formule produite de mani re exponentielle cf duplication du Z Il existe d autres algorithmes 9 Logiciel libre disponible sur http www cs uni potsdam de clasp ou comme paquet Ubuntu d un d p t universe 10 Cet environnement est affich sous la forme d une liste de litt raux dans laquelle une variable n gative a la valeur f et une variable positive a la valeur t un nom de variable ne pouvant appara tre qu au plus une fois dans la liste 11 http en wikipedia org wiki DPLL_algorithm 2014 2015 page 8 14 Ensimag 1A App TP intro aux traitements des langages qui produisent des formules de taille lin aire ils ne sont pas tr s compliqu s mais hors du cadre de ce TP Ici on se contente donc de consid rer des formules initiales dont la NNF est une CNF Ce cadre est suffisant pour traiter les formules g n r es sur les sudokus Concr tement clasp attends sur son entr e standard une formule CNF au format DIMACS On fournit ici une m thode printDimacs dans la classe Nnf qui effectue l affichage de la formule dans ce format si celle ci est une CNF et qui l ve une exception sinon public void printDimacs La t che 4 consiste donc utiliser le script sudoku sh qui utilise les fichiers Java clasp pour r soudre des grilles de sudoku Ce
20. ode next qui d place la t te de lecture jusqu au prochain lex me et le retourne public Token next Ici un lex me abstrait sp cial joue le r le de sentinelle de fin de fichier il ne correspond aucun lex me concret et sert uniquement exprimer que la lecture du fichier d entr e est finie Un lex me abstrait de type Token cf profil ci dessous correspond donc soit la sentinelle de fin dans ce cas l attribut code vaut la valeur Token EOF soit un nom de variable dans ce cas la m thode isVar r pond true et le nom de la variable est obtenu par la m thode getVarO soit un caract re ASCII dans ce cas la m thode isVar r pond false et l attribut code vaut le code ASCII du caract re Voil le profil de la classe Token Code ex cut par java ea Lexer l public class Token Lexer lexer new Lexer public boolean isVar Token curr lexer next public int getVar while curr code Token EUF public final int code System out println curr static final int EOF 1 curr lexer next 6 2 Principe de l analyse syntaxique en notation pr fixe L analyseur syntaxique invoque donc la m thode next du lexer pour construire AST au fur et mesure de la lecture du fichier d entr e la suite des lex mes n est donc pas stock e en m moire et la 13 c est dire dans la m thode main de Lexer 2014 2015 pa
21. que op ration Or Prop x Prop Prop ou constante du langage ais ment identifiable Implies Prop x Prop Prop partir du nom du constructeur e g True pour t Var Pos Prop et And pour amp Le cas le moins vident est celui de Var utilis pour repr senter les variables Ici Pos est qualifi e de sorte externe la signature ne dit pas comment fabriquer des l ments de ce type on suppose qu on sait le faire par ailleurs Tandis que Prop est une sorte interne On ne peut fabriquer des arbres de type Prop qu en utilisant les constructeurs de la signature Avec cette notation l arbre associ l exemple introductif t amp 1 gt 2 s crit Implies And True Var 1 Neg V ar 2 Une fa on de coder cette signature en Java est donn e par le squelette de classe ci dessous La casse a t ici adapt e de mani re respecter les conventions de programmation Java La sorte Prop est repr sent e par une classe public abstract class Prop Prop tandis que Pos est repr sent e abusivement final static public Prop TRUE par int Les constructeurs sans arguments sont final static public Prop FALSE cod s comme des constantes Java Le construc public Prop neg public Prop and Prop public Prop or Prop public Prop implies Prop static public Prop var int teur Var qui n a pas d argument de sorte Prop est repr sent par une m thode statique Les autres constructeurs sont repr
22. que tous ces tests passent essayez un test plus cons quent en lan ant le script suivant pour afficher le mode d emploi lancer ce script sans option testparser_sudoku sh prefix Celui ci teste le parser sur la r gle du jeu du Sudoku pour afficher le mode d emploi complet lancer ce script sans option Essayer d abord avec Sudoku rn 2 Si a marche essayez avec Sudoku rn 3 pour v rifier le passage l chelle de votre parser 14 Autrement dit la suite u des lex mes qui restent lire apr s l appel r cursif v rifie u v u 15 Comme cette m thode fonctionne peu pr s vous pouvez commencer par impl menter recParse et ne corriger Lexer que dans un deuxi me temps Impl menter recParse vous aidera comprendre ce que doit faire Lexer 2014 2015 page 11 14 Ensimag 1A App TP intro aux traitements des langages 7 T che 6 analyse syntaxique en notation infixe Pour cet analyseur on r utilise le lexer d fini en section 6 1 Le fonctionnement de l analyseur va donc fortement ressembler celui d crit en section 6 2 mais pour une syntaxe concr te plus complexe Pour crire ce parser il faut commencer par effectuer une s rie de transformations de BNF partir de la sp cification initiale du parser donn e en 7 1 Ici il faut s appuyer sur les concepts vus en cours qui ne sont pas r d taill s ici Pr cisons qu il existe des outils pour faire ces transformations automatiquement
23. r e vous pouvez lancer la commande ci dessous qui affiche en notation infixe la formule avant sa mise en NNF java ea Sudoku DebugSolver lt nom_de_grille Lorsque le script fonctionne pour les sudokus de taille 4 vous pouvez essayer ceux de taille 9 en positionnant dans le fichier Sudoku java la constante rn 3 et en recompilant 6 T che 5 analyse syntaxique en notation pr fixe La section 1 3 d crit la m thode printPrefix qui affiche un AST de type Prop en notation pr fixe La t che 5 consiste programmer un analyseur syntaxique qui r alise en gros la r ciproque d tecter si une suite de caract res sur l entr e standard correspond un AST de type Prop en notation pr fixe et dans ce cas retourner cet AST sinon lever une erreur La syntaxe reconnue par l analyseur autorise des commentaires ceux ci commencent par le caract re 4 et se terminent en fin de ligne Elle autorise un nombre arbitraires de blancs caract re espace ou tabulation ou retour la ligne entre les mots consituants la formule Dans la suite on d signe ces mots sous le vocable de lex mes ou tokens en anglais Un tel lex me est donc soit un nom de variable constitu d une suite de chiffres en base 10 soit un caract re parmi amp gt tf Des exemples de fichiers en notation pr fixe sont donn s dans le sous r pertoire prefix Les fichiers commen ant par ok_ doivent tre accept s par l analyseur alors qu
24. rilles sont valides except celles en sudoku4 ko o le num ro en suffixe est inf rieur ou gal 4 Les grilles sudoku4 ko5 et sudoku4 ko6 sont valides mais sans solution 3 T che 2 syntaxe des formules en forme normale n gative En section 4 on impl mente un algorithme l mentaire de simplification des formules proposition nelles essentiellement cette simplification consiste liminer les constantes t et f et l op rateur gt et propager les n gations jusqu aux feuilles de AST sous jacent les noms de variable Au pr alable dans cette section on s int resse une forme de formules simplifi es appel e forme normale n gative ou NNF acronyme de Negative Normal Form Plus pr cis ment une formule Prop est en NNF si et seulement si elle n a pas de sous formule stricte syntaxiquement constante mais la formule elle m me peut tre r duite une constante et elle ne contient pas l op rateur binaire gt et chaque op rateur s applique directement un nom de variable Ainsi l exemple introductif n est pas une NNF Mais il a une NNF logiquement quivalente 1 2 Dans la suite de cette section on d finit une sorte d AST appel e Nnf qui repr sente tr s exactement la syntaxe des formules NNF On emploie pour cela la m me d marche que celle d crite en section 1 La t che 2 consiste impl menter la traduction des AST de sorte Nnf en A
25. rises depuis la fin des ann es 1960 L objectif du cours de p riode 2 est de pr senter une de ces solutions parmi les plus simples Mais avant d en arriver l on va commencer par se placer en aval de l analyse syntaxique c est dire en supposant que celle ci a d j t r alis e On commence donc par tudier le r sultat de l analyseur syntaxique lorsque gt la suite de caract res en entr e correspond bien une formule syntaxiquement amp AO N M correcte Ce r sultat est un arbre appel arbre de syntaxe abstraite dessin TON t 1 2 ci contre qui repr sente la structure du parenth sage de la formule Ainsi les diff rents concepts de TL qu on va illustrer au travers de ce TP programm en Java sont par ordre d apparition les arbres de syntaxe abstraite ou AST pour Abstract Syntax Trees en sections 1 et 3 l valuation d expression ou interpr tation d expression en section 2 la compilation au sens d une traduction d une structure d AST en une autre structure d AST en sections 3 et 4 l analyse syntaxique en notation pr fixe en section 6 et l analyse syntaxique en notation infixe via une grammaire hors contexte LL 1 en section 7 La prise en main des fichiers Java fournis est d taill e dans l annexe section 8 1 La notion d AST illustr e sur les formules propositionnelles On introduit une notation math matique pour d finir les AST ind pendam
26. script commence par afficher la grille d entr e Il passe alors clasp une formule exprimant la conjonction de la formule produite par initSudokuPuzzle voir section 1 2 et d une formule exprimant les contraintes de la grille d entr e S il n y a pas de solution il s arr te Sinon il affiche la grille correspondant la solution trouv e par clasp Puis il effectue un deuxi me appel clasp en lui passant une formule qui est la conjonction de la formule pr c dente et la n gation de la solution trouv e par clasp on peut ainsi v rifier qu il n y a qu une solution pour la grille d entr e conform ment aux usages Sinon cette deuxi me solution est affich e En utilisant la commande sudoku sh nom_de_grille pour une taille de sudoku n 4 effectuez les v rifications list es ci dessous 1 il y a au moins deux solutions pour la grille sudoku4 vide 2 il n y a aucune solution sur la grille sudoku4 ko 3 il y a une seule solution sur la grille sudoku4 2169 En cas de comportement diff rent votre algorithme de mise en NNF est vraisemblablement faux Il faut alors le d boguer avant de faire de nouveaux essais de r solution de sudoku il est conseill de cr er pour cela de nouveaux petits cas de tests dans la classe Test plut t que d essayer de d boguer directement l aide des grosses formules de sudokus N anmoins si vous souhaitez avoir une id e de la formule d ent
27. tantes les variables et les parenth ses sont au niveau de pr c dence 0 tous les niveaux de pr c dences sont associatifs droite 7 2 A faire transformer la BNF en une BNF non ambigu Votre premier travail consiste crire une BNF attribu e non ambigu qui reconnaisse le m me langage que celle donn e en section 7 1 et qui pour chaque mot de ce langage synth tise le m me AST lorsqu on restreint la BNF 7 1 aux arbres d analyse qui satisfont les r gles de pr c dence 2014 2015 page 12 14 Ensimag 1A App TP intro aux traitements des langages Pour exprimer les contraintes de pr c dence comme des r gles de BNF il faut introduire un non terminal P par niveau de pr c dence n avec 0 lt n lt 3 o chaque non terminal a la signification suivante La langage reconnu par P est l ensemble des mots u reconnus par le P de la BNF en 7 1 tels que pour tout sous mot v de u contenant un op rateur de niveau de pr c dence strictement sup rieure n il existe un sur mot v de v tel que v est un sous mot de u qui est reconnu par P Ainsi P3 correspond l ensemble des mots reconnus par P et donc est l axiome de votre BNF Et pour 0 lt n lt 3 on a Pa C P 1 De plus si u1 et u2 sont dans P alors un mot de la forme uy ug peut tre reconnu par P2 condition que u1 et uz soient eux m mes dans P2 mais pas par P On ne demande pas de prouver ce niveau que la BNF o
28. u sh infix d abord avec Sudoku rn 2 puis Sudoku rn 3 8 Annexe prise en main des fichiers Java fournis Avant de lancer une premi re ex cution Java des sources fournies situ es dans le sous r pertoire src il faut 1 Compiler en lan ant ant Son makefile est donn dans build xml Il place les fichiers class produits dans le sous r pertoire bin 2 Positionner correctement la variable CLASSPATH en lan ant simplement source prelude sh Ex cuter la machine virtuelle java avec l option ea pour v rifier l ex cution les assertions ins truction assert pr sentes dans le code Pour chercher le nom des classes ventuellement ex cutables pensez faire ls bin 2014 2015 page 13 14 Ensimag 1A App TP intro aux traitements des langages 8 1 dition des fichiers Java Vous pouvez diter les fichiers Java avec votre diteur favori directement dans le sous r pertoire src Pour compiler il faut utiliser ant la racine du r pertoire fourni comme expliqu ci dessus Vous pouvez aussi diter compiler les fichiers sous eclipse Il suffit de lancer eclipse amp en ligne de commande puis de s lectionner le menu File New gt Project Java Project puis de d cocher l option Use default location puis de s lectionner le r pertoire fourni via le bouton Browse priori l organisation du r pertoire est alors compatible avec les options par d faut
29. ule exprime la r gle que sur la grille un nombre p donn de 1 n appara t au plus une fois par ligne au plus une fois par colonne et au plus une fois par sous r gion Vn x y n Cette formule contient donc O n4 connecteurs logiques il serait fastidieux de l crire la main En section 2 on utilise le r sultat de initSudokuRule pour v rifier qu une grille de sudoku stock e dans un fichier respecte ces contraintes En section 5 on s int resse la r solution des puzzles de sudoku on utilise pour cela la formule retourn e par initSudokuPuzzle qui exprime quelle condition une grille est une solution d un puzzle Cette formule est simplement obtenue comme le et logique de la formule retourn e par initSudokuRule et de la formule exprimant que toute case de la grille contient au moins un nombre p de 1 n 1 3 Patron de conception interpr teur en Java La classe Prop est impl ment e par l interm diaire de sous classes dont la hi rarchie suit la signature multisort e ci dessus Ce style de programmation OO s appelle patron de conception interpr teur Chaque sorte interne ici il n y a que Prop correspond une classe abstraite Et chaque constructeur de la signature ayant un type S1 x x Sn Sh11 correspond une classe concr te qui h rite de la classe correspondant Sh 1 a une liste d attributs de type S1 Sn 3 cfhttp en wikipedia org wiki Interpreter_pattern 2014
30. ur correspondant au constructeur exemple True pour t et And pour amp puis les fils r cursivement donc avec un parcours en profondeur On fait un cas particulier pour le constructeur Var pour lequel on n affiche que le fils Dans le cas de l exemple introductif on obtient ainsi gt amp t 1 2 5 Voir ci dessous le code de cette m thode dans les sous classes And et Var class And extends Prop class Var extends Prop void printPrefix void printPrefix System out print u amp System out print left printPrefix value right printPrefix F 2 T che 1 valuation des formules propositionnelles Cette t che consiste programmer un valuateur ou interpr teur des formules propositionnelles Concr tement il s agit d tendre la classe Prop avec une m thode eval en respectant le principe du patron interpr teur d crit en section 1 3 abstract public boolean eval Environment env 4 Ici on simplifie un peu le code vis vis du fichier fourni Dans celui ci printPrefix r alise un affichage indent plus lisible ce qu on ne fait pas ici 5 C est donc tr s similaire la notation sans parenth se de PAST 2014 2015 page 4 14 Ensimag 1A App TP intro aux traitements des langages tant donn un environnement c est dire une fonction associant une valeur bool enne chaque nom de variables l valuation d une formule X est
Download Pdf Manuals
Related Search