Abstract FR:

Nous presentons un cadre de conception d'analyseurs dynamiques et d'analyseurs statiques a partir de specifications operationnelles. Nous proposons des specifications d'analyseurs en deux parties : la semantique du langage de programmation considere et la definition de la propriete recherchee. Nous considerons le cadre de la semantique naturelle pour la definition du langage de programmation. Ces semantiques presentent un double avantage : elles sont a la fois compositionnelles et intentionnelles. Les proprietes sont definies comme des fonctions sur les arbres de preuves de la semantique. Celles qui ne sont pas specifiques a un langage donne peuvent ainsi etre definies une fois pour toutes et specialisees pour des langages particuliers. La composition de la semantique et de la propriete definit une analyse dynamique a posteriori ; il s'agit en effet d'une fonction qui calcule dans un premier temps la trace d'execution (arbre de preuve) complete d'un programme avant d'en extraire la propriete recherchee. Des transformations de programmes permettent d'obtenir une definition recursive autonome de l'analyseur. Cette fonction est en fait un analyseur dynamique a la volee dans le sens ou il calcule la propriete recherchee au fur et a mesure de l'execution du programme. On realise ensuite une abstraction de cet analyseur pour obtenir un analyseur statique : on applique pour ce faire la theorie de l'interpretation abstraite. Nous illustrons notre cadre a l'aide d'exemples d'analyses specifiques comme la duree de vie d'un langage imperatif et l'analyse de necessite d'un langage fonctionnel d'ordre superieur. Nous montrons aussi comment une analyse d'interet general, en l'occurrence le filtrage de programmes, peut etre definie sur un format de semantique, puis instanciee a differents langages.