A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts

This paper outlines a sound and complete Hoare logic for a sequential object-oriented language with inheritance and subtyping like Java. It describes a weakest precondition calculus for assignments and object-creation, as well as Hoare rules for reasoning about (mutually recursive) method invocations with dynamic binding. Our approach enasoning at an abstraction level that coincides with the general ion level of object-oriented languages.

• Type: Conference
• Year: 2003
• Where: FMOODS
• Authors: Cees Pierik, Frank S. de Boer
• Keywords: Complete Hoare Logic, FMOODS 2003, FMOODS 2007, Object-oriented Languages, Weakest Precondition Calculus