The essential part of an abstract interpretation framework is to build a machine-representable abstract lattice expressing interesting properties about the states possibly reached by a program at run-time. Many techniques have been developed that take for granted that one knows in advance the class of properties that must be expressible in the abstract framework. There are cases however when there are no a priori indications about the relative interest of such classes. Loosely put, the approximate lattice itself can be seen as one of the results of the computation. We expose a method, called dynamic partitioning, that can be used in such cases to build an interesting, rich approximate framework from an original and supposedly poor one. We study two techniques. The first one, called basic partitioning, can be used when the original framework consists in a lattice A. We show that using a well chosen subset of A one can define a partial order and a monotonic concretization function over this subset such that nontrivial safe approximations of the least fixed point of any continuous function can be computed with the help of a generalized widening operator. In order to justify this technique, we shall generalize the classical lattice oriented framework developed by the Cousots to cases where no Galois connection can be defined between general partial orders. The second technique, called functional partitioning, can be used to finitely approximate functions in C -> B, when C is a set and B is a lattice. This approximation requires that an original upper approximation of the lattice P(C) be defined and assigns different meanings to well chosen subsets of A*B. Finally, we show that this technique can be applied with great benefits to several classical situations encountered in interprocedural abstract interpretation.
[PostScript, PDF, © 1992 Cambridge University Press]