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].
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. In: Formal Aspects of Computing
Kassios, Y.: A Theory of Object Oriented Refinement. PhD thesis, University of Toronto (2006)
Kassios, Y.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Formal Methods (2006)
Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: Marktoberdorf Summer School Lecture Notes (2006)
Barnett, M., DeLine, R., Fahndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6) (2004)
Jacobs, B., Piessens, F.: Verification of programs with inspector methods. In: FTFJP (2006)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversität Hagen (2001)
Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: ICSE (1996)
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, Springer, Heidelberg (2004)
Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, Springer, Heidelberg (2004)
Jacobs, B., Piessens, F.: Inspector methods for state abstraction. Journal of Object Technology 6(5) (2007)
Darvas, A., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, Springer, Heidelberg (2007)
Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)
Parkinson, M.: Local Reasoning for Java. PhD thesis, University of Cambridge (2005)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)
Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: PLDI (2002)
Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. (Unpublished, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smans, J., Jacobs, B., Piessens, F., Schulte, W. (2008). An Automatic Verifier for Java-Like Programs Based on Dynamic Frames. In: Fiadeiro, J.L., Inverardi, P. (eds) Fundamental Approaches to Software Engineering. FASE 2008. Lecture Notes in Computer Science, vol 4961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78743-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-78743-3_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78742-6
Online ISBN: 978-3-540-78743-3
eBook Packages: Computer ScienceComputer Science (R0)