Analyse statique modulaire des langages à objet.

We presented a framework for the modular analysis of object-oriented languages. We defined a liberal and generic trace semantics for class-bases object-oriented languages and we proved it sound and complete w.r.t. a trace semantics for object-oriented programs. We derived systematically the equations characterizing class invariants as an abstraction of the class concrete semantics. We dealt with the three main features of object-oriented languages: – inheritance, by considering the analysis of subclasses without accessing the parent's class source; – polymorphism, by studying an effective notion of behavioral subtyping; – encapsulation, by abstracting the interactions between an object and its context using regular expressions. The framework is very flexible and in particular we can distinguish three orthogonal axes for the analysis: – abstract domain: a class can be analyzed using either a generic abstract domain (Chapters 6 and 5) or a symbolic relational domain (Chapter 7) to obtain a more efficient analysis; – inheritance: a subclass can be analyzed either directly, by expanding the subclass relation, or indirectly, by using the parent's invariant (Chapters 8 and 9); – context: a class can be analyzed either aside from the instantiation context, so to obtain a result valid for all the contexts, or using an approximation of the context itself (Chapter 10). The future work will include the implementation and the study of the practical aspects of our results. In particular the interest will be the exploration of the orthogonal axes of the analysis. Furthermore, we plan to extend the results in order to cope with aspect-oriented languages [38], with concurrency and with temporal properties of objects.Dans la thèse nous présentons un cadre pour l'analyse statique de langages orientés objets qui tient compte des propriétés de modularité de ces langages. Il y a plusieurs défis à relever pour obtenir une analyse statique efficace de langages orientés objet. Tout d'abord, elle doit gérer les particularités de ces langages telles que l'héritage, le polymorphisme et la résolution de méthodes virtuelles. Deuxièmement, elle doit être modulaire. En fait, les programmes orientés objet typiques sont fait de plusieurs milliers de classes et une analyse monolithique du programmes complet peut être trop coûteuse pour être pratiquée. Troisièmement, la technologie orientée objet favorise la programmation par composants, en cela qu'un composant (une classe) est développée une fois pour toute et utilisée dans de nombreux contextes différents. Aussi, une analyse statique efficace doit pouvoir inférée des propriétés des composants valides pour toutes les instantiations possibles de contextes. Dans cette thèse, nous présentons une analyse qui relève les défis esquissés ci-dessus. En particulier, nous nous concentrons sur une analyse qui peut inférer des invariants de classe. Un invariant de classe est une propriété d'une classe valide pour chaque instanciation, avant et après l'exécution de n'importe quelle méthode de la classe. Notre analyse a plusieurs avantages. Elle est indépendante du langage, elle exploite la structure modulaire des langages orientés objet et elle gère les principales fonctionnalités de ces langages, à savoir l'héritage, le polymorphisme et l'encapsulation. Le cadre présenté dans cette thèse est très flexible. En particulier, il permet de régler finement l'analyse selon les trois axes orthogonaux suivants: - Domaine abstrait sous-jacent: une classe peut être analysée en utilisant soit un domaine abstrait générique soit un domaine abstrait symbolique de façon à obtenir une analyse plus efficace mais moins précise. - Gestion de l'héritage: une sous-classe peut être analysée soit directement, en expansant syntaxiquement la relation de sous-classe, soit indirectement, en utilisant l'invariant du parent afin d'éviter une explosion quadratique de la complexité. -Traitement des contextes d'instantiation: une classe peut être utilisée soit indépendamment du contexte, afin d'obtenir un résultat valable dans tous les contextes, soit en utilisant une approximation du contexte afin d'obtenir un résultat plus précis mais moins général