Title: An automatic verifier for Java-like programs based on dynamic frames
Authors: Smans, Jan ×
Jacobs, Bart
Piessens, Frank
Schulte, Wolfram #
Issue Date: Apr-2008
Publisher: Springer
Series Title: Lecture Notes in Computer Science vol:4961 pages:261-275
Conference: Fundamental Approaches to Software Engineering location:Budapest, Hungary date:March 29 - April 6 2008
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. The verifier itself and the examples shown in this paper can be downloaded from the authors’ homepage [1].
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
fulltext.pdf Published 464KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science