Runtime Verification of Object Invariants with Guarantee

High level design decisions are never captured formally in programs and are often violated as programs evolve. In this paper, we focus on design decisions in which an object o works correctly only if another object p is in some specific states. Such decisions can be specified as the object invariant of o.

The invariant of o must hold when control is not inside any of o’s methods (i.e. when o is in a steady state). From discussion forums on widely used APIs, it is clear that there are many instances where o’s invariant is violated by the programmer inadvertently changing the state of p when o is in a steady state. Typically, o and p are objects exposed by the API, and the programmer (who is the user of the API), unaware of the dependency between o and p, calls a method of p in such a way that o’s invariant is violated. The fact that the violation occurred is detected much later, when a method of o is called again, and it is dicult to determine exactly where such violations occur.

We propose a runtime verication scheme which guarantees that when o is in a steady state, any violation of o’s invariant is detected exactly where it occurs. This is done by tracking dependencies automatically and validating whether a state change of an object p breaks the invariant of any object o that depends on p. We demonstrate that our tool InvCOP, which implements this scheme, can accurately pinpoint violations of invariants involving multiple objects that were reported in discussion forums on widely used APIs.