Graph-based object-oriented Hoare Logic

Abstract

We are happy to contribute to this volume of essays in honor of He Jifeng on the occasion of his 70th birthday. This work combines and extends two recent pieces of work that He Jifeng has made significant contributions: the rCOS Relational Semantics of Object-Oriented Programs [4] and the Trace Model for Pointers and Objects [7]. It presents a graph-based Hoare Logic that deals with most general constructs of object-oriented (oo) programs such as assignment, object creation, local variable declaration and (possibly recursive) method invocation. The logic is built on a graph-based operational semantics of oo programs so that assertions are formalized as properties on graphs of execution states. We believe the logic is simple because 1) the use of graphs provides an intuitive visualization of states and executions of oo programs and thus it is helpful in thinking of and formulating clear specifications, 2) the logic follows almost the whole traditional Hoare Logic and the only exception is the backward substitution law which is not valid for oo programs, and 3) the mechanical implementation of the logic would not be much more difficult than traditional Hoare Logic. Despite the simplicity, the logic is powerful enough to reason about important oo properties such as aliasing and reachability. © 2013 Springer-Verlag.