A Logical Account of Hoare’s Mismatch Information Hiding via Second Order Framing in Region Logic

We investigate information hiding in object-based programs and the associated mismatch. While client reasoning is in terms of in-terface specifications, the implementation of an interface is verified against different specifications that involve invariants about inter-nal data structures. Soundness of this mismatched reasoning de-pends on encapsulation of internal data structures. The problem is that encapsulation is notoriously difficult to achieve in contempo-rary software in which shared mutable objects are ubiquitous. We account for the mismatch via proof rules that phrase the mismatch using explicit conditions that are imposed on client effects. Effects are tracked using ghost state and separation assertions in a style that has been used in a number of verification tools. Our approach per-mits the formulation of encapsulation disciplines (such as owner-ship, or package confinement) as part of the interface specification, in the form of a dynamic boundary, rather than as a discipline di-rectly baked into a verifier. One implication is that we can provide a foundation for the axiomatic semantics of these verifiers. Our ap-proach is flexible in that disciplines can be used on a per-module basis and then combined to achieve end to end soundness. 1