Skip to main content
SpringerLink
Log in
Book cover

European Conference on Object-Oriented Programming

ECOOP 2011: ECOOP 2011 – Object-Oriented Programming pp 358–382Cite as

Verifying Multi-object Invariants with Relationships

  • Conference paper

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

Abstract

Relationships capture the interplay between classes in object-oriented programs, and various extensions of object-oriented programming languages allow the programmer to explicitly express relationships. This paper discusses how relationships facilitate the verification of multi-object invariants. We develop a visible states verification technique for Rumer, a relationship-based programming language, and demonstrate our technique on the Composite pattern. The verification technique leverages the “Matryoshka Principle” embodied in the Rumer language: relationships impose a stratification of classes and relationships (with corresponding restrictions on writes to fields, the expression of invariants, and method invocations). The Matryoshka Principle guarantees the absence of transitive call-backs and restores a visible states semantics for multi-object invariants. As a consequence, the modular verification of multi-object invariants is possible.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Hoare, C.: Proof of correctness of data representations. Acta Inf. 1(4), 271–281 (1972)

    Article  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

  4. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev29, Iowa State University (2006)

    Google Scholar 

  5. Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  6. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Leino, K 3(6), 27–56 (2004)

    Google Scholar 

  7. Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Barnett, M., Naumann, J.D.A.: 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)

    Chapter  Google Scholar 

  9. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program 62(3), 253–286 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  10. Leino, K.R.M., Schulte, W.: Using history invariants to verify observers. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 80–94. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. 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  MATH  Google Scholar 

  12. Summers, A.J., Drossopoulou, S.: Considerate Reasoning and the Composite Design Pattern. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 328–344. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  13. Spitzen, J.M., Wegbreit, B.: The verification and synthesis of data structures. Acta Inf. 4(2), 27–144 (1975)

    Article  MATH  Google Scholar 

  14. Guttag, J.V.: Notes on type abstraction (version 2). IEEE Trans. Software Eng. 6(1), 13–23 (1980)

    Article  Google Scholar 

  15. Parkinson, M.J.: Class invariants: The end of the road? In: IWACO (2007)

    Google Scholar 

  16. Rumbaugh, J.: Relations as semantic constructs in an object-oriented language. In: OOPSLA, vol. 481, pp. 466–481. ACM, New York (1987)

    Google Scholar 

  17. Albano, A., Ghelli, G., Orsini, R.: A relationship mechanism for a strongly typed object-oriented database programming language. In: VLDB, pp. 565–575. Morgan Kaufmann, San Francisco (1991)

    Google Scholar 

  18. Bierman, G., Wren, A.: First-class relationships in an object-oriented language. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 262–286. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Pearce, D.J., Noble, J.: Relationship aspects. In: AOSD, pp. 75–86. ACM, New York (2006)

    Chapter  Google Scholar 

  20. Balzer, S., Gross, T.R., Eugster, P.T.: A relational model of object collaborations and its use in reasoning about relationships. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 323–346. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  21. Wren, A.: Relationships for Object-oriented Programming Languages. PhD thesis, University of Cambridge (November 2007)

    Google Scholar 

  22. Østerbye, K.: Design of a class library for association relationships. In: LCSD (2007)

    Google Scholar 

  23. Bodden, E., Shaikh, R., Hendren, L.: Relational aspects as tracematches. In: AOSD, pp. 84–95. ACM, New York (2008)

    Chapter  Google Scholar 

  24. Nelson, S., Pearce, D.J., Noble, J.: First class relationships for OO languages. In: MPOOL (2008)

    Google Scholar 

  25. Balzer, S., Gross, T.R.: Modular reasoning about invariants over shared state with interposed data members. In: PLPV, pp. 49–56. ACM, New York (2010)

    Google Scholar 

  26. Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput. 19(2), 159–189 (2007)

    Article  MATH  Google Scholar 

  27. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)

    MATH  Google Scholar 

  28. Bierhoff, K., Aldrich, J.: Permissions to specify the Composite design patterns. In: SAVCBS, pp. 89–94 (2008)

    Google Scholar 

  29. Jacobs, B., Smans, J., Piessens, F.: Verifying the Composite pattern using separation logic. In: SAVCBS, pp. 83–88 (2008)

    Google Scholar 

  30. Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  31. Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for exible alias protection. In: OOPSLA, pp. 48–64. ACM, New York (1998)

    Google Scholar 

  32. Dietl, W.: Universe Types Topology, Encapsulation, Genericity, and Tools. PhD thesis, ETH Zurich, 18522 (2009)

    Google Scholar 

  33. Bierman, G.M., Meijer, E., Torgersen, M.: Lost in translation: Formalizing proposed extensions to C#. In: OOPSLA, pp. 479–498. ACM, New York (2007)

    Google Scholar 

  34. Drossopoulou, S., Francalanza, A., Müller, P., Summers, A.: A Unified Framework for Verification Techniques for Object Invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 412–437. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  35. Balzer, S.: A relationship-based programming language and its value for program verification. Technical report, ETH Zurich (2011)

    Google Scholar 

  36. Summers, A.J., Drossopoulou, S., Müller, P.: Universe-type-based verification techniques for mutable static fields and methods. JOT 8(4), 85–125 (2009)

    Article  Google Scholar 

  37. Parkinson, M.J.: Local Reasoning for Java. PhD thesis, University of Cambridge (2005)

    Google Scholar 

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

    Google Scholar 

  39. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  40. Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  41. Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 387–411. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  42. Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zurich, Switzerland

    Stephanie Balzer & Thomas R. Gross

Authors
  1. Stephanie Balzer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas R. Gross
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Software Technology group, Technische Universität, Darmstadt, Germany

    Mira Mezini

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Balzer, S., Gross, T.R. (2011). Verifying Multi-object Invariants with Relationships. In: Mezini, M. (eds) ECOOP 2011 – Object-Oriented Programming. ECOOP 2011. Lecture Notes in Computer Science, vol 6813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22655-7_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22655-7_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22654-0

  • Online ISBN: 978-3-642-22655-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation