Towards client-aware interface specifications
Henrique Rebêlo · 2011
Runtime assertion checking (RAC) is a well-established technique for runtime verification of object-oriented (OO) programs. Contemporary RACs use specifications from the receiver's dynamic type when checking method calls. This implies that in presence of subtyping and dynamic dispatch features of object-oriented programming, these specifications differ from the ones used by static verification tools, which rely on the specifications associated with the static type of the receiver. Besides the heterogeneity problem, this also hinders the benefits of modular reasoning achieved by the notion of supertype abstraction. In this context, we propose a more precise runtime assertion checking for OO programs that better matches the semantics used in static verification tools. While we describe our approach, we discuss how it can be used to avoid the heterogenous semantics problem and among others.