Abstract
Model fields are specification-only fields that encode abstractions of the concrete state of a data structure. They allow specifications to describe the behavior of object-oriented programs without exposing implementation details.
This paper presents a sound verification methodology for model fields that handles object-oriented features, supports data abstraction, and can be applied to a variety of realistic programs. The key innovation of the methodology is a novel encoding of model fields, where updates of the concrete state do not automatically change the values of model fields. Model fields are updated only by a special pack statement. The methodology guarantees that the specified relation between a model field and the concrete state of an object holds whenever the object is valid, that is, is known to satisfy its invariant.
The methodology also improves on previous work in three significant ways: First, the formalization of model fields prevents unsoundness, even if an interface specification is inconsistent. Second, the methodology fully supports inheritance. Third, the methodology enables modular reasoning about frame properties without using explicit dependencies, which are not handled well by automatic theorem provers.
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
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. JOT 3(6) (2004)
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, pp. 49–69. Springer, Heidelberg (2005)
Barnett, M., Naumann, D.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)
Breunesse, C.-B., Poll, E.: Verifying JML specifications with model fields. In: Formal Techniques for Java-like Programs, pp. 51–60 (2003); Tech. Rep. 408, ETH Zurich
Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Software—Practice & Experience 35(6), 583–599 (2005)
Cok, D., Kiniry, J.R.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Tech. Rep. HPL-2003-148, HP Labs (July 2003)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. JOT 4(8) (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, vol. 37(5) in SIGPLAN Notices, pp. 234–245. ACM, New York (2002)
Hoare, C.A.R.: Proofs of correctness of data representation. Acta Inf. 1, 271–281 (1972)
Jacobs, B., Piessens, F.: Verifying programs using inspector methods for state abstraction. Tech. Rep. CW 432, Dept. of Comp. Sci., K. U. Leuven (December 2005)
Kassios, Y.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. Tech. Rep. CSRG-528, U. of Toronto, Comp. Sys. Research Group (July 2005)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev28, Iowa State University, Department of Computer Science (2003), See www.jmlspecs.org
Rustan, K., Leino, M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology (1995)
Rustan, K., Leino, M.: Data groups: Specifying the modification of extended state. In: OOPSLA, vol. 33(10) in SIGPLAN Notices, pp. 144–153. ACM, New York (1998)
Rustan, K., Leino, M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency & Computation: Practice & Experience 15, 117–154 (2003)
Naumann, D., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: LICS, pp. 313–323. IEEE, Los Alamitos (2004)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268–280. ACM, New York (2004)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247–258. ACM, New York (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leino, K.R.M., Müller, P. (2006). A Verification Methodology for Model Fields. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_9
Download citation
DOI: https://doi.org/10.1007/11693024_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)