🚀 go-pugleaf

Soutenance de th�se, Val�rie Gouranton :

jeudi 11 septembre 1997 � 10h30, salle M�tivier, Irisa.



D�rivation d'analyseurs dynamiques et statiques � partir de
sp�cifications op�rationnelles.


Jury :

MM. :	Jean-Pierre Ban�tre	Pr�sident
        Dominique Bolignano     Rapporteur
        Thomas Jensen           Examinateur
       	Daniel Le M�tayer       Directeur de th�se
        David Schmidt           Rapporteur



R�sum� :

Nous pr�sentons un cadre de conception d'analyseurs dynamiques et
d'analyseurs statiques � partir de sp�cifications op�rationnelles. 
Nous proposons des sp�cifications d'analyseurs en deux parties : 
la s�mantique du langage de programmation consid�r� et la d�finition 
de la propri�t� recherch�e.

Nous consid�rons le cadre de la s�mantique naturelle pour la
d�finition du langage de programmation. Ces s�mantiques pr�sentent un
double avantage : elles sont � la fois compositionnelles et
intentionnelles. Les propri�t�s sont d�finies comme des fonctions sur
les arbres de preuves de la s�mantique.  Celles qui ne sont pas
sp�cifiques � un langage donn� peuvent ainsi �tre d�finies une fois
pour toutes et sp�cialis�es pour des langages particuliers.

La composition de la s�mantique et de la propri�t� d�finit une analyse
dynamique a posteriori ; il s'agit en effet d'une fonction qui
calcule dans un premier temps la trace d'ex�cution (arbre de preuve)
compl�te d'un programme avant d'en extraire la propri�t� recherch�e.
Des transformations de programmes permettent d'obtenir une d�finition
r�cursive autonome de l'analyseur.  Cette fonction est en fait un
analyseur dynamique � la vol�e dans le sens o� il calcule la
propri�t� recherch�e au fur et � mesure de l'ex�cution du
programme. On r�alise ensuite une abstraction de cet analyseur pour
obtenir un analyseur statique : on applique pour ce faire la th�orie
de l'interpr�tation abstraite.

Nous illustrons notre cadre � l'aide d'exemples d'analyses sp�cifiques
comme la dur�e de vie d'un langage imp�ratif et l'analyse de n�cessit�
d'un langage fonctionnel d'ordre sup�rieur. Nous montrons aussi
comment une analyse d'int�r�t g�n�ral, en l'occurrence le filtrage de
programmes, peut �tre d�finie sur un format de s�mantique, puis
instanci�e � diff�rents langages.


Mots cl�s : analyse dynamique, analyse statique, s�mantique
naturelle, transformation de programmes, interpr�tation abstraite,
analyse de dur�e de vie, analyse de n�cessit�,
filtrage de programmes.




Abstract :

We present a framework for designing  dynamic and static analysers from
operational specifications.  The analyser specification has two
components : a semantics of the programming language under
consideration and a definition of the property that the analysis is
supposed to return. From a program and a semantics definition of a 
property, we derive a system of recursive equations whose solution is
an
approximation of the property under consideration. 
For the programming language
definition we use the natural semantics because this kind of
semantics is both intentional and compositional. Properties are
expressed as functions on semantics derivation trees. Properties 
that are not
specific to a language can be defined once for all and instantiated
to particular languages.

A dynamic analyser is expressed as composition of a semantics function
and a property. The analyser is called a posteriori, it is a
function computing first a complete program execution trace
(derivation tree) and then extracting the property of interest.  An
autonomous recursive definition of an analyser can be obtained by
program transformation.  This function is a dynamic on the
fly analyser that computes the property during 
program execution. A static analyser is obtained by abstract
interpretation of the dynamic on the fly analyser.

Our framework is illustrated with specific analyses like live variable
analysis for an imperative language and neededness analysis for a
higher order functional language.  We show how a general analysis like
slicing can be defined in our semantics format and instantiated to
specific languages.



Keywords : dynamic analysis, static analysis, natural
semantics, program transformation, abstract interpretation,
live variables analysis, neededness analysis,
slicing analysis.




Vous �tes �galement les bienvenus au pot qui suivra.


--
Moderation de fr.announce.seminaires + Annonces: fr-sem@frmug.org
-- 
--
http://www.freenet.fr/villemin/