Enforcing Object Protocols by Combining Static and Dynamic Analysis - Gopinathan, Madhu; Rajamani, Sriram (ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA), 2008)
In this paper, we consider object protocols that constrain interactions between objects in a program. Several such protocols have been proposed in the literature [3, 9, 6, 5]. For many APIs (such as JDOM [23], JDBC [22]), API designers constrain how API clients interact with API objects. In practice, API clients violate such constraints, as evidenced by postings in discussion forums for these APIs. Thus, it is important that API designers specify constraints using appropriate object protocols and enforce them. The goal of an object protocol is expressed as a protocol in variant. Fundamental properties such as ownership can be expressed as protocol invariants. We present a language, PROLANG, to specify object protocols along with their protocol invariants, and a tool, INVCOP++, to check if a program satisﬁes a protocol invariant. INVCOP++ separates the problem of checking if a protocol satisﬁes its protocol invariant (called protocol correctness), from the problem of checking if a program conforms to a protocol (called program conformance). The former is solved using static analysis, and the latter using runtime analysis. Due to this separation (1) errors made in protocol design are detected at a higher level of abstraction, independent of the program’s source code, and (2) performance of conformance checking is improved as protocol correctness has been veriﬁed statically. We present theoretical guarantees about the way we combine static and runtime analysis, and empirical evidence that our tool INVCOP++ ﬁnds usage errors in widely used APIs. We also show that statically checking protocol correctness greatly optimizes the overhead of checking program conformance, thus enabling API clients to test whether their programs use the API as intended by the API designer.