Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Validity Invariants and Effects

  • Conference paper
ECOOP 2007 – Object-Oriented Programming (ECOOP 2007)

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

Included in the following conference series:

Abstract

Object invariants describe the consistency of object states, and are crucial for reasoning about the correctness of object-oriented programs. However, reasoning about object invariants in the presence of object abstraction and encapsulation, arbitrary object aliasing and re-entrant method calls, is difficult.

We present a framework for reasoning about object invariants based on a behavioural contract that specifies two sets: the validity invariant—objects that must be valid before and after the behaviour; and the validity effect—objects that may be invalidated during the behaviour. The overlap of these two sets is critical because it captures precisely those objects that need to be re-validated at the end of the behaviour. When there is no overlap, no further validity checking is required.

We also present a type system based on this framework using ownership types to confine dependencies for object invariants. In order to track the validity invariant, the type system restricts updates to permissible contexts, even in the presence of re-entrant calls. Object referencing and read access are unrestricted, unlike earlier ownership type systems.

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. Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, Springer, Heidelberg (2004)

    Google Scholar 

  2. Almeida, P.S.: Balloon types: Controlling sharing of state in data types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 32–59. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  3. Barnett, M., DeLine, R., Fahndrich, M., Leino, K., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)

    Google Scholar 

  4. Barnett, M., Naumann, D.: Friends need a bit more: Maintaining invariants over shared state. In: Mathematics of Program Construction, pp. 54–84 (2004)

    Google Scholar 

  5. Birka, A., Ernst, M.D.: A practical type system and language for reference immutability. In: OOPSLA ’04. Proceedings of the 19th annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 35–49. ACM Press, New York (2004)

    Chapter  Google Scholar 

  6. Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102–126 (2000)

    Google Scholar 

  7. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pp. 259–270 (2005)

    Google Scholar 

  8. Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 213–223. ACM Press, New York (2003)

    Chapter  Google Scholar 

  9. Clarke, D.: Object Ownership and Containment. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia (2001)

    Google Scholar 

  10. Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and disjointness of type and effect. In: 17th Annual Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (November 2002)

    Google Scholar 

  11. Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 48–64. ACM Press, New York (1998)

    Chapter  Google Scholar 

  13. Dietl, W., Muller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT) (2005)

    Google Scholar 

  14. Hogg, J.: Islands: aliasing protection in object-oriented languages. In: OOPSLA ’91. Proceedings of Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 271–285. ACM Press, New York (1991)

    Chapter  Google Scholar 

  15. Ishtiaq, S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. In: Proceedings of the 28th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, ACM Press, New York (2001)

    Google Scholar 

  16. Leavens, G.: Modular specification and verification of object-oriented programs. Software 8(4), 72–80 (1991)

    Article  Google Scholar 

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

  18. Lu, Y., Potter, J.: On ownership and accessibility. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 99–123. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Lu, Y., Potter, J.: Protecting representation with effect encapsulation. In: Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York (2006)

    Google Scholar 

  20. Meyer, B.: Eiffel: the language. Prentice-Hall, Inc, Upper Saddle River, NJ, USA (1992)

    MATH  Google Scholar 

  21. Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Upper Saddle River, NJ, USA (1997)

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  23. Müller, P., Poetzsch-Heffter, A.: Universes: A type system for controlling representation exposure. In: Programming Languages and Fundamentals of Programming (1999)

    Google Scholar 

  24. Müller, P., Poetzsch-Heffter, A.: Universes: A Type System for Alias and Dependency Control. Fernuniv. Fachbereich Informatik (2001)

    Google Scholar 

  25. Müller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen (2001)

    Google Scholar 

  26. Muller, P., Poetzsch-Heffter, A., Leavens, G.: Modular invariants for layered object structures. Science of Computer Programming (2006)

    Google Scholar 

  27. Naumann, D., Barnett, M.: Towards imperative modules: reasoning about invariants and sharing of mutable state. In: Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium, pp. 313–323 (2004)

    Google Scholar 

  28. Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: 2002. Proceedings. 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74 (2002)

    Google Scholar 

  30. Schulte, W.: Towards a Verifying Compiler: The Spec# Approach. Microsoft Research (2006), http://research.microsoft.com/specsharp/

Download references

Author information

Authors and Affiliations

  1. Programming Languages and Compilers Group, School of Computer Science and Engineering, University of New South Wales, Sydney,  

    Yi Lu, John Potter & Jingling Xue

Authors
  1. Yi Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Potter
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jingling Xue
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Erik Ernst

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lu, Y., Potter, J., Xue, J. (2007). Validity Invariants and Effects. In: Ernst, E. (eds) ECOOP 2007 – Object-Oriented Programming. ECOOP 2007. Lecture Notes in Computer Science, vol 4609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73589-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-73589-2_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-73588-5

  • Online ISBN: 978-3-540-73589-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation