Contracts as a support to static analysis of open systems
Résumé
Static analysis is a powerful tool to establish various properties of programs. The analysis is often directed by the call graph of the programs (e.g [3]) and thus is not well suited to open object-oriented systems, or sometimes consider that when a method is called, all its parameter escape to any control (e.g. [1]). In this work in progress, we introduce the notion of contract as a support to openness and extensibility: we propose an analysis computing the contract of a method relying on contracts of methods used by it, and respecting the requirements of the methods using it. Thus the analysis is compositional and the properties of composed code can be deduced from contract composition. We give two examples of applications in the context of open object-oriented systems and dynamic loading of applications: one for a distributed Wcet computation method for small embedded systems and one for computation of information flows in Java pro- grams. These examples allow us to present two types of contracts: the contracts that are introduced by the designer of the system, and the contracts that are automatically computed by the analysis with regard to the first ones.