This is a long paper: 67 pages plus a 21-page appendix. It describes the verification of a dynamically dispatched method call of an object-oriented program by using supertype abstraction. The authors maintain that such abstraction is only valid when each subtype in the program is a behavioral subtype. The goal of this paper is to prove that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. In order to do this, the authors semantically formalize supertype abstraction and behavioral subtyping for a Java-like sequential language.

The paper first provides a detailed formal definition of supertype abstraction and behavioral subtyping, followed by a section on related work. The Java-like language is then presented, followed by an overview of formal method specification, modular verification, and modular correctness, which is subsequently used to develop predicate transformer semantics.

Finally, behavioral subtyping and its equivalence to supertype abstraction are presented, along with how behavioral subtyping is ensured through specification inheritance and an adaption of the results to partial correctness. The appendix provides additional proofs and ancillary definitions.

The paper is well organized and presented with more than 80 references. It is intended for those doing serious object-oriented programming language research. The authors have at least 40 years of experience in this area and appear to be primarily addressing their peers (to which I can definitely recommend this work). However, graduate students should probably seek guidance from their advisors before attempting to read an advanced paper of this type.