Inferring Object Invariants

The program state for object-oriented languages, such as Java or C#, consists of both variables local to procedures and variables stored in the global heap. The variables stored in the heap are the fields of objects (i.e., fields of class instances). This paper proposes a technique for inferring properties of such object-oriented programs. The technique divides the work into two interacting parts: a flow-sensitive analysis that tracks the local and global state as seen at each particular program point, and a flow-insensitive analysis that tracks properties that are common among all “valid” instances of a class, independent of the program counter. The analysis is sound and works in the presence of many object references (aliasing). For precision, the analysis makes use of a recent methodology for object invariants, which makes explicit when each object's invariant is supposed to hold (valid objects) or is allowed to be violated.