Automatic Inference of Class Invariants
Abstract:
In this paper we address the problem of performing a class static
analysis in a modular fashion, i.e. by just analyzing the
class code and not the full program. In particular we show two things:
the first one is how starting from a class C we can derive an
approximation C' to be used either as a class documentation or
as a tester for a client using C; the second one is how to
discover, in a fully automatic way, a class invariant. Two methods for
class invariant computation are presented, proved correct and their
usage is discussed.
Back to the Homepage