How to Cook a Complete Hoare Logic for Your Pet OO Language

摘要

This paper introduces a general methodology for obtaining complete Hoare logics for object-oriented languages. The methodology is based on a new completeness result of a Hoare logic for a procedural language with dynamically allocated variables. This new result involves a generalization of Gorelick's seminal completeness result of the standard Hoare logic for recursive procedures with simple variables. We show how this completeness result can be generalized to existing Hoare logics for typical object-oriented concepts like method calls, sub-typing and inheritance, and dynamic binding, by transforming an encoding of these concepts into this procedural language with dynamically allocated variables.