Skip to main content
SpringerLink
Log in

Assertion-Based Encapsulation, Object Invariants and Simulations

  • Conference paper
Formal Methods for Components and Objects (FMCO 2004)

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

Included in the following conference series:

Abstract

In object-oriented programming, reentrant method invocations and shared references make it difficult to achieve adequate encapsulation for sound modular reasoning. This tutorial paper surveys recent progress using auxiliary state (ghost fields) to describe and achieve encapsulation. Encapsulation is assessed in terms of modular reasoning about invariants and simulations.

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

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, pp. 1–25. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM (2002) (Accepted, revision pending. Extended version of [3])

    Google Scholar 

  3. Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 166–177 (2002)

    Google Scholar 

  4. Banerjee, A., Naumann, D.A.: State based ownership, reentrance, and encapsulation. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 387–411. Springer, Heidelberg (2005) (to appear)

    Chapter  Google Scholar 

  5. Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004) (Special issue: ECOOP 2003 workshop on Formal Techniques for Java-like Programs)

    Article  Google Scholar 

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

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

    Google Scholar 

  8. Bierman, G., Parkinson, M.: Separation logic and abstraction. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 247–258 (2005)

    Google Scholar 

  9. Birkedal, L., Torp-Smith, N.: Higher order separation logic and abstraction (Febraury 2005) (submitted)

    Google Scholar 

  10. Borba, P., Sampaio, A., Cavalcanti, A., Cornélio, M.: Algebraic reasoning for object-oriented programming. Sci. Comput. Programming 52(1-3), 53–100 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  11. Borba, P.H.M., Sampaio, A.C.A., Cornélio, M.L.: A refinement algebra for object-oriented programming. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 457–482. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA (2002)

    Google Scholar 

  13. Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 213–223 (2003)

    Google Scholar 

  14. Calcagno, C., O’Hearn, P., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Comput. Sci. 298(3), 557–581 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  15. Cavalcanti, A.L.C., Naumann, D.A.: Forward simulation for data refinement of classes. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 471–490. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Clarke, D.: Object ownership and containment. Dissertation, Computer Science and Engineering, University of New South Wales, Australia (2001)

    Google Scholar 

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

    Chapter  Google Scholar 

  18. de Boer, F., Pierik, C.: Computer-aided specification and verification of annotated object-oriented programs. In: Jacobs, B., Rensink, A. (eds.) Formal Methods for Open Object-Based Distributed Systems, pp. 163–177 (2002)

    Google Scholar 

  19. de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  20. DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: ACM Conf. on Program. Lang. Design and Implementation (PLDI), pp. 59–69 (2001)

    Google Scholar 

  21. Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep exposure. Research 156, DEC Systems Research Center (1998)

    Google Scholar 

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

    Google Scholar 

  23. Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf 1, 271–281 (1972)

    Article  MATH  Google Scholar 

  24. Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202–219. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Jacobs, B., Leino, K.R.M., Schulte, W.: Multithreaded object-oriented programs with invariants. In: SAVCBS (2004)

    Google Scholar 

  26. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 262–284. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  28. Leino, K.R.M., Müller, P.: Modular verification of static class invariants. In: Formal Methods (2005)

    Google Scholar 

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

    MATH  Google Scholar 

  30. Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst. 16(6) (1994)

    Google Scholar 

  31. Lynch, N., Vaandrager, F.: Forward and backward simulations part I: Untimed systems. Information and Computation 121(2) (1995)

    Google Scholar 

  32. Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)

    MATH  Google Scholar 

  33. Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of Second Intl. Joint Conf. on Artificial Intelligence, pp. 481–489 (1971)

    Google Scholar 

  34. Mitchell, J.C.: Representation independence and data abstraction. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 263–276 (1986)

    Google Scholar 

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

    Book  MATH  Google Scholar 

  36. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Technical Report 424, Department of Computer Science, ETH Zurich (2004)

    Google Scholar 

  37. Naumann, D.A.: Ideal models for pointwise relational and state-free imperative programming. In: Sondergaard, H. (ed.) ACM International Conference on Principles and Practice of Declarative Programming, pp. 4–15 (2001)

    Google Scholar 

  38. Naumann, D.A.: Patterns and lax lambda laws for relational and imperative programming. Technical Report 2001-2, Computer Science, Stevens Institute of Technology (2001)

    Google Scholar 

  39. Naumann, D.A.: Soundness of data refinement for a higher order imperative language. Theoretical Comput. Sci. 278(1-2), 271–301 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  40. Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: IEEE Symp. on Logic in Computer Science (LICS), pp. 313–323 (2004)

    Google Scholar 

  41. O’Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 268–280 (2004)

    Google Scholar 

  42. O’Hearn, P.W., Tennent, R.D.: Parametricity and local variables. Journal of the ACM 42(3), 658–709 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  43. Pierik, C., Clarke, D., de Boer, F.S.: Controlling object allocation using creation guards. In: Formal Methods 2005 (2005)

    Google Scholar 

  44. Pierik, C., de Boer, F.: On behavioral subtyping and completeness. In: ECOOP Workshop on Formal Techniques for Java-like Programs (2005) (to appear)

    Google Scholar 

  45. Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theoretical Comput. Sci. (2005) (to appear)

    Google Scholar 

  46. Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algol-Like Languages, vol. 2, ch. 17, pp. 173–193. Birkhauser, Basel (1997); Reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, Brunswick, NJ (July 1996), pp. 152–163 (1996)

    Google Scholar 

  47. Pitts, A.M.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 321–359 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  48. Plotkin, G.: Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence (1973)

    Google Scholar 

  49. Rehof, Mogensen: Tractable constraints in finite semilattices. Sci. Comput. Programming (1996)

    Google Scholar 

  50. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  51. Skalka, C., Smith, S.: Static use-based object confinement. Springer International Journal of Information Security 4(1-2) (2005)

    Google Scholar 

  52. Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming, 2nd edn. ACM Press and Addison-Wesley, New York (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stevens Institute of Technology, Hoboken, NJ, 07030, USA

    David A. Naumann

Authors
  1. David A. Naumann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI, Kruislaan 413, 1098, Amsterdam, SJ, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300, Leiden, RA, The Netherlands

    Marcello M. Bonsangue

  3. Centre Equitation, VERIMAG, 2 Avenue de Vignate, 38610, Grenoble-Gières, France

    Susanne Graf

  4. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University Kiel, Hermann-Rodewald-Straße 3, 24118, Kiel, Germany

    Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Naumann, D.A. (2005). Assertion-Based Encapsulation, Object Invariants and Simulations. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2004. Lecture Notes in Computer Science, vol 3657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11561163_11

Download citation

  • DOI: https://doi.org/10.1007/11561163_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29131-2

  • Online ISBN: 978-3-540-31939-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation