Verification of programs using inspector methods
Bart Jacobs, Frank Piessens · Formal Techniques for Java-like Programs · 2006
Most classes in an object-oriented program provide access to an object’s state through methods, so that client code does not depend on and cannot interfere with the object’s internal representation composed of fields and internal component objects. Methods used for this purpose are sometimes called inspector methods. In order to extend the benefits of inspector methods to specifications, the method contracts of non-inspector methods may be expressed using inspector methods, hence providing support for state abstraction in specifications. In this paper, we propose an approach to the verification of programs that use inspector methods in method contracts and object invariants. Inspector methods may have parameters, and they may depend on the state of objects passed as arguments. Our approach builds on the Boogie methodology for object invariants and ownership. Performing state abstraction in a programming language that allows aliasing through object references poses a framing problem. Specifically, client code needs to be able to tell whether modifying a given object or calling a given method may affect the value of a given inspector method call. We solve this by modeling inspector methods as functions that take as arguments only those parts of the heap on which they depend. Thanks to a novel logical encoding of the heap, we can do this without breaking information hiding, even in cases where inspector methods depend on internal component objects. The core of our approach has been implemented in a custom build of the Spec# program verifier.