Contexte
Au cours des derniers mois, dans l'équipe WAM, nous avons mis au point le premier solveur au monde capable de résoudre des problèmes d'analyse statique de taille réelle sur des programmes manipulant des données XML. Le solveur permet de vérifier automatiquement des propriétés sur les arbres, comme la navigation sous contrainte de type. Il permet de raisonner avec des requêtes XPath et des types XML (DTDs, XML Schemas, ...), qui sont aujourd'hui des constructions de première classe dans la plupart des langages de manipulation de structures XML (ex: XSLT, XQuery, XJ, XDuce, etc.)
Le solveur permet par exemple de déterminer automatiquement si deux requêtes XPath sont équivalentes pour une infinité de documents sur lequel elles peuvent être évaluées. Ceci est très utile pour l'optimisation de programmes: il devient en effet possible de substituer une requête par sa version optimisée statiquement dans un programme, sans risque, afin d'améliorer les performances à l'exécution, par exemple.
Le solveur permet en réalité de résoudre toute une classe de problèmes d'analyse statique mettant en jeu des types d'arbres réguliers et des requêtes régulières (par exemple: le typage statique de requêtes, l'inclusion de types XML...). Ceci permet par exemple de s'assurer de la compatibilité ascendante lors de l'évolution de formats de données structurées, ou encore de bâtir de nouveaux langages de programmation statiquement typés...
Cette avancée repose sur la conception d'une nouvelle logique d'arbre, également élaborée dans le projet WAM [2]. Cette logique offre à ce jour le meilleur compromis connu entre puissance expressive et efficacité pour raisonner sur des arbres (la complexité de sa procédure de décision a été prouvée optimale).
Description du stage
Le solveur que nous avons mis au point ouvre la voie à une nouvelle classe d'analyseurs statiques, encore inenvisageable il y a peu. Comme ce solveur est le premier de sa catégorie, il n'existe à ce jour aucune base de comparaison pour ce type d'analyses statiques.
L'objectif du stage est de concevoir un tel référentiel. Ce référentiel pourra prendre la forme d'un ensemble de tests de propriétés sur les arbres, qui seraient exprimés dans la logique, ou bien avec les constructions XML de plus haut niveau. Les propriétés seront méticuleusement choisies, par exemple par exploration des limites du solveur, étude et synthèse de cas concrets, état de l'art des cas problématiques pour les méthodes antérieures, etc. Ces tests seront exprimés à l'aide d'un vocabulaire XML approprié (il sera possible de définir un langage XML générique à cet effet). Ces résultats seront accompagnés d'une implantation permettant le test automatisé avec vérification par rapport au référentiel établi. Cette librairie sera implanté en JAVA et interfacé directement avec le solveur.
Ce stage comporte une composante théorique (compréhension et utilisation d'une logique modale interprétée sur les arbres), appliquée (développement Java, XML) et une partie exploratoire sur une problématique en plein essor (le solveur se situe à la pointe ce qu'il est possible de faire actuellement en analyse statique de programmes XML). Ce stage offre un bon positionnement pour une éventuelle poursuite en thèse.
Références
[1] Static Analysis of XML Programs, Pierre Genevès and Nabil Layaïda, (invited article) in ERCIM news number 72: "The Future Web", 2008, http://ercim-news.ercim.org/content/view/326/536/
[2] Efficient Static Analysis of XML Paths and Types, Pierre Genevès and Nabil Layaïda and Alan Schmitt, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2007
[3] A System for the Static Analysis of XPath, Pierre Genevès and Nabil Layaïda, ACM Transactions on Information Systems (TOIS), Volume 24, Number 4, October 2006