Skip to main content
SpringerLink
Log in

A Unified Framework for Verification Techniques for Object Invariants

  • Conference paper
Book cover ECOOP 2008 – Object-Oriented Programming (ECOOP 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5142))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS. LNCS, pp. 49–69. Springer, Heidelberg (2005)

    Google Scholar 

  3. 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)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. JOT 4(8), 5–32 (2005)

    Google Scholar 

  7. Drossopoulou, S., Francalanza, A., Müller, P.: A unified framework for verification techniques for object invariants. In: FOOL (2008)

    Google Scholar 

  8. 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

    Google Scholar 

  9. Fähndrich, M., Xia, S.: Establishing object invariants with delayed types. In: OOPSLA, pp. 337–350. ACM Press, New York (2007)

    Google Scholar 

  10. Flanagan, C., Qadeer, S.: A Type and Effect System for Atomicity. In: PLDI, pp. 338–349. ACM Press, New York (2003)

    Google Scholar 

  11. 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)

    Google Scholar 

  12. Hoare, C.A.R.: Proofs of correctness of data representation. Acta Informatica 1, 271–281 (1972)

    Article  MATH  Google Scholar 

  13. Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM 17(10), 549–557 (1974)

    Article  MATH  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Google Scholar 

  17. 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

  18. 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)

    Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)

    MATH  Google Scholar 

  21. Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM ToPLAS 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  22. Lu, Y., Potter, J.: Soundness of Oval. Priv. Commun. (June 2007)

    Google Scholar 

  23. 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)

    Chapter  Google Scholar 

  24. Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs (1988)

    Google Scholar 

  25. Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)

    MATH  Google Scholar 

  26. Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Invariants for non-hierarchical object structures. Electr. Notes Theor. Comput. Sci. 195, 211–229 (2008)

    Article  Google Scholar 

  27. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  28. Parkinson, M.: Class invariants: the end of the road? In: International Workshop on Aliasing, Confinement and Ownership (2007)

    Google Scholar 

  29. Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247–258. ACM Press, New York (2005)

    Google Scholar 

  30. Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: POPL, pp. 75–86. ACM Press, New York (2008)

    Google Scholar 

  31. Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (1997)

    Google Scholar 

  32. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  33. Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. In: LICS, pp. 162–173. IEEE Computer Society Press, Los Alamitos (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Imperial College London,  

    S. Drossopoulou & A. J. Summers

  2. University of Southampton,  

    A. Francalanza

  3. Microsoft Research, Redmond,  

    P. Müller

Authors
  1. S. Drossopoulou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. P. Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. J. Summers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Vitek

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation