Dans cette thèse, on présente un cadre théorique général d'analyse statique pour l'inférence de propriétés `structurelles' ou d'`usage' des programmes. Le terme `structurel', emprunté à la théorie de la démonstration, suggère un rapport étroit avec la logique linéaire, où les règles structurelles de contraction et affaiblissement jouent un rôle important. Le problème de l'analyse statique consiste à trouver une traduction d'un langage source dans le style de PCF vers un langage comportant des annotations structurelles. On montre que l'on peut characteriser l'ensemble de traductions possibles comme des solutions d'un ensemble d'inequations appropriées. Plus particulièrement, on s'intéresse à la plus petite solution, qui correspond à la traduction la plus précise ou optimale. La plus grande partie de ce manuscrit de thèse est dédié à un seul cas d'étude, l'analyse linéaire, dont l'objectif est de déterminer les valeurs qui sont utilisées une seule fois. On decrit d'abord une version de l'analyse linéaire très simplifiée, en suite on introduise des extensions qui comportent des notions de sous-typage et du polymorphisme d'annotations, ce étant clé dans la pratique, car il permet à l'analyse de garder son pouvoir expressif en présence de modules compilés séparément.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00010369 |
| Date | 27 May 2005 |
| Creators | Alberti, Francisco |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0022 seconds