Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection

Inheritance and method overriding are crucial concepts in object-oriented programming (OOP) languages. These concepts support a hierarchy of classes that reuse common data and methods. Most existing works for OO verification focus on modular reasoning in which they could support dynamic dispatching and thus efficiently enforce the Liskov substitution principle on behavioural subtyping. They are based on superclass abstraction to reason about the correctness of OO programs. However, techniques to reason about the incorrectness of OOP are yet to be investigated. In this paper, we present a mechanism that 1) specifies the normal and abnormal executions of OO programs by using ok specifications and er specifications respectively; 2) verifies these specifications by a novel under-approximation proof system based on incorrectness logic that can support dynamic modularity. We introduce subclass reflection with dynamic views and an adapted subtyping relation for under-approximation. Our proposal can deal with both OOP aspects (e.g., behavioural subtyping and casting) and under-approximation aspects (e.g., dropping paths). To demonstrate how the proposed proof system can soundly verify the specifications, we prove its soundness, prototype the proof system, and report on experimental results. The results show that our system can precisely reason about the incorrectness of programs with OOP aspects, such as proving the presence of casting errors and null-pointer-exceptions.