An Automatic Verifier for Java-Like Programs Based on Dynamic Frames

Jan Smans, Bart Jacobs 0002, Frank Piessens, and Wolfram Schulte

Abstract

Data abstraction is crucial in the construction of modular programs, since it ensures that internal changes in one module do not propagate to other modules. In object-oriented programs, classes typically enforce data abstraction by providing access to their internal state only through methods. By using method calls in method contracts, data abstraction can be extended to specifications. In this paper, methods used for this purpose must be side-effect free, and are called pure methods. We present an approach to the automatic verification of object-oriented programs that use pure methods for data abstraction. The cornerstone of our approach is the solution to the framing problem, i.e. client code must be able to determine whether state changes affect the return values of pure methods. More specifically, we extend each method contract with a method footprint, an upper bound on the memory locations read or written by the corresponding method. Footprints are specified using dynamic frames, special pure methods that return sets of memory locations. Thanks to this abstraction, implementations can evolve independently from specifications, loosely coupled only by pure functions. We implemented this approach in a custom build of the Spec# program verifier, and used it to automatically verify several challenging programs, including the iterator and observer patterns.

Details

Publication typeInproceedings
Published inFASE
Pages261-275
Volume4961
SeriesLecture Notes in Computer Science
ISBN978-3-540-78742-6
PublisherSpringer
> Publications > An Automatic Verifier for Java-Like Programs Based on Dynamic Frames