Résumé : 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éralIntroduction
Motivations
Object-oriented Languages
Verification and Optimization
Modularity
Abstract Interpretation
Results
Static Analysis of Classes
Introductory Example
Main Results
Overview of the Thesis
Preliminaries
Notation and Basic Definitions
Partial Orders
Functions and Fixpoints
Traces
Abstract Interpretation
Galois Connections
Fixpoint Approximation
Chaotic and Asynchronous Iterations
Concrete Semantics
Semantics of Object-oriented Languages in Literature
Types
Object Calculi
Abstract State Machines
Denotational Semantics
Whole-Program Trace Semantics
Syntax
Semantic Domains
Whole-Program Semantics
Class Trace Semantics
Constructor and Methods Semantics
Object Semantics
Class Semantics
Relation between the Two Semantics
Abstraction
Soundness and Completeness of the Class Semantics
Languages with Class Destructor
Abstract Semantics
Stepwise Abstraction
First Abstraction: Collecting Traces
Abstract Domain
Abstraction
Abstract Semantics
Second Abstraction: Reachable States
Abstract Domain
Abstraction
Abstract Semantics
Inference of Class Invariants
Overview of Class Invariants
Class Invariants in the Literature
Design by Contract
Java Modeling Language
Assertions in Java and .net
Daikon
ESC/Java and Houdini
Some Static Analyses for Object Oriented Languages
Automatic Inference of Class Invariants
Strongest State-based Class Invariant
Abstraction
A Bank Account Example
Abstract Domain
Fixpoint Computation
Escaping Scope
Fixpoint Computation and Complexity
Modularity and Program Analysis
Discussion
Symbolic Relations for the Approximation of Set of Traces
Relational Symbolic Abstract Domains
Module Abstraction by Relations
Constraints
Concretization of Constraints
Variables Dropping
Abstract Domain Operations
Analysis and Soundness
Instantiations of the A-domain
Types
Relevant Context Inference
Incremental Modular Analysis
Discussion
Symbolic Relations for Approximating the Class Semantics
Introduction
An Example of Stack
First Abstraction: Approximating Classes
Definition of an Abstract Class
Applications
Checking the Well-behavior of a Client
Soundness
Second Abstraction: Class Invariants
History-insensitive Class Invariant
History-sensitive Class Invariant
On comparing the I and J Invariants
Discussion
Class Invariants in Presence of Inheritance
Inheritance
Inheritance in Software Development
Inheritance in Programming Languages
Semantics of Inheritance
Inheritance and Class Invariants
An Example of Stack with Undo
Non-Modular Analysis
Subclass Expansion
Analysis of the Expanded Class
Modular Analysis
Class Extension
Methods refining
Symbolic Relations and Inheritance
Discussion
Static Analysis-based Inheritance
Behavioral Subtyping
Examples
Class Hierarchy
Systematic Refinement of the Class Hierarchy
Modular Verification
Observables
Domain of Observables
Subclassing through Observables
Static Checking of Behavioral Subtyping
Modular Verification
Domain Refinement
Application to the Examples
Discussion
Context Approximation
Introduction
Context Syntax and Semantics
Syntax
Semantics
Collecting Semantics
Monolithic Abstract Semantics
Abstract Semantic Domains
Abstract Object Semantics
Monolithic Abstract Context Semantics
Separate Abstract Semantics
Regular Expressions Domain
Interaction History
Separate Object Analysis
Separate Context Analysis
Putting It All Together
Discussion
Conclusions
Bibliography