A Relational Program Logic with Data Abstraction and Dynamic Framing

In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extended to encompass dynamically allocated objects. In recent years, progress has been made towards formalizing the claim, for simulation, though mainly in semantic developments. In this paper, the ideas are combined with the idea in Hoare's 1969 paper: a logic of programs. For a language with dynamically allocated shared mutable objects, we introduce a relational Hoare logic that formalizes encapsulation, hiding of invariants, and relating two implementations via coupling relations. Relations and other assertions are expressed in first order logic. Specifications can express a wide range of relational properties such as conditional equivalence and noninterference with declassification. The proof rules facilitate reasoning by means of convenient alignments and are shown sound with respect to a conventional operational semantics. Applicability to representative examples of data abstraction is demonstrated using an SMT-based implementation.