Wenhua, Li; Le, Quang Loc; Song, Yahui; Chin, Wei-Ngan; (2023) Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection. In: Programming Languages and Systems. APLAS 2023. Springer: Singapore, Singapore.

Preview

Text il-oop-aplas2023.pdf - Other Download (447kB) | Preview

Abstract

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 execution OO programs by using ok specifications and er specifications respectively; 2) verifies the specifications by a novel underapproximation 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 lossless 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 nullpointer-exceptions.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as CSVXMLJSON

Archive Staff Only

View Item