Abstract
Object invariants define the consistency of objects. They have subtle semantics because of call-backs, multi-object invariants and subclassing. Several visible-state verification techniques for object invariants have been proposed. It is difficult to compare these techniques and ascertain their soundness because of differences in restrictions on programs and invariants, in the use of advanced type systems (e.g. ownership types), in the meaning of invariants, and in proof obligations.
We develop a unified framework for such techniques. We distil seven parameters that characterise a verification technique, and identify sufficient conditions on these parameters which guarantee soundness. We instantiate our framework with three verification techniques from the literature, and use it to assess soundness and compare expressiveness.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. JOT 3(6), 27–56 (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS. LNCS, 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)
Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL, pp. 87–99. ACM Press, New York (2008)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA, vol. 33(10), pp. 48–64. ACM Press, New York (1998)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. JOT 4(8), 5–32 (2005)
Drossopoulou, S., Francalanza, A., Müller, P.: A unified framework for verification techniques for object invariants. In: FOOL (2008)
Drossopoulou, S., Francalanza, A., Müller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 412–437. Springer, Heidelberg (2008), http://www.doc.ic.ac.uk/~ajs300m/papers/frameworkFull.pdf
Fähndrich, M., Xia, S.: Establishing object invariants with delayed types. In: OOPSLA, pp. 337–350. ACM Press, New York (2007)
Flanagan, C., Qadeer, S.: A Type and Effect System for Atomicity. In: PLDI, pp. 338–349. ACM Press, New York (2003)
Hähnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 151–171. Springer, Heidelberg (2005)
Hoare, C.A.R.: Proofs of correctness of data representation. Acta Informatica 1, 271–281 (1972)
Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM 17(10), 549–557 (1974)
Huizing, K., Kuiper, R.: Verification of object-oriented programs using class invariants. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol. 1783, pp. 208–221. Springer, Heidelberg (2000)
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14–26. ACM Press, New York (2001)
Leavens, G.T., Müller, P.: Information hiding and visibility in interface specifications. In: ICSE, pp. 385–395. IEEE Computer Society Press, Los Alamitos (2007)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Department of Computer Science, Iowa State University (February 2007), http://www.jmlspecs.org
Leino, K.R.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., Schulte, W.: Using history invariants to verify observers. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)
Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM ToPLAS 16(6), 1811–1841 (1994)
Lu, Y., Potter, J.: Soundness of Oval. Priv. Commun. (June 2007)
Lu, Y., Potter, J., Xue, J.: Object Invariants and Effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 202–226. Springer, Heidelberg (2007)
Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs (1988)
Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)
Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Invariants for non-hierarchical object structures. Electr. Notes Theor. Comput. Sci. 195, 211–229 (2008)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006)
Parkinson, M.: Class invariants: the end of the road? In: International Workshop on Aliasing, Confinement and Ownership (2007)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247–258. ACM Press, New York (2005)
Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: POPL, pp. 75–86. ACM Press, New York (2008)
Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (1997)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)
Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. In: LICS, pp. 162–173. IEEE Computer Society Press, Los Alamitos (1992)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drossopoulou, S., Francalanza, A., Müller, P., Summers, A.J. (2008). A Unified Framework for Verification Techniques for Object Invariants. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-70592-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70591-8
Online ISBN: 978-3-540-70592-5
eBook Packages: Computer ScienceComputer Science (R0)