Skip to main content
SpringerLink
Log in

Modular Specification of Encapsulated Object-Oriented Components

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

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 4111))

Included in the following conference series:

Abstract

A well-defined boundary of components allows to encapsulate internal state and to distinguish between internal calls that remain inside the component and external calls that have target objects outside the component. From a static point of view, such boundaries define the programmer’s interface to the component. In particular, they define the methods that can be called on the component. From a dynamic point of view, the boundaries separate the component state and those parts of the program state outside the component.

In this tutorial paper, we investigate encapsulated components that are realized based on object-oriented concepts. We define a semantics that captures a flexible notion of hierarchical encapsulation with confined references. The semantics generalizes the encapsulation concepts of ownership types. It is used as a foundation for modular behavioral component specifications. In particular, it allows to provide a simple semantics for invariants and an alternative solution for the frame problem. We demonstrate this new specification methodology by typical programming patterns.

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. Ábrahám, E., Bonsangue, M.M., de Boer, F.S., Grüner, A., Steffen, M.: Observability, connectivity, and replay in a sequential calculus of classes. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 296–316. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky [29], pp. 1–25

    Google Scholar 

  3. Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 166–177. ACM Press, New York (2002)

    Chapter  Google Scholar 

  4. Barnett, M., Naumann, 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 

  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) (2004)

    Google Scholar 

  6. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA 2002 [30], pp. 211–230

    Google Scholar 

  7. Büchi, M.: Safe Language Mechanisms for Modularization and Concurrency. PhD thesis, Turku Centre for Computer Science (May 2000)

    Google Scholar 

  8. Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales (July 2001)

    Google Scholar 

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

    Chapter  Google Scholar 

  10. DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky [29], pp. 465–490

    Google Scholar 

  11. Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)

    Article  Google Scholar 

  12. Dietl, W., Müller, P., Poetzsch-Heffter, A.: A type system for checking applet isolation in Java Card. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 129–150. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer’s reduction semantics for classes and mixins. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 241–269. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Gosling, J., Joy, B., Steele, G., Bracha, G.: The JavaTM Language Specification, 2nd edn. Addison-Wesley, Reading (2000)

    Google Scholar 

  15. Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification. In: Texts and Monographs in Computer Science. Springer, Heidelberg (1993)

    Google Scholar 

  16. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems (TOPLAS) 23(3), 396–450 (2001)

    Article  Google Scholar 

  17. Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, ch. 12, pp. 175–188. Kluwer, Dordrecht (1999)

    Google Scholar 

  18. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML. Technical Report No. 98-06z, Iowa State University (2004)

    Google Scholar 

  19. Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky [29], pp. 491–516.

    Google Scholar 

  20. Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems (TOPLAS) 24(5), 491–553 (2002)

    Article  Google Scholar 

  21. Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation (PLDI 2002), pp. 246–257. ACM Press, New York (2002)

    Chapter  Google Scholar 

  22. Microsoft. C# Language Specification (2001)

    Google Scholar 

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

    Book  MATH  Google Scholar 

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

    Google Scholar 

  25. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience 15(2), 117–154 (2003)

    Article  MATH  Google Scholar 

  26. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Technical Report 424, ETH Zürich, Chair of Software Engineering (2005)

    Google Scholar 

  27. Naumann, D.A.: Assertion-based encapsulation, object invariants and simulations. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 251–273. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

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

  29. Odersky, M. (ed.): ECOOP 2004. LNCS, vol. 3086. Springer, Heidelberg (2004)

    Google Scholar 

  30. Proceedings of the 17th ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications (OOPSLA 2002). ACM Press, New York (2002)

    Google Scholar 

  31. Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitationsschrift, Technische Universität München (1997)

    Google Scholar 

  32. Pucella, R.: Towards a formalization for COM part I: the primitive calculus. In: OOPSLA 2002 [30], pp. 331–342 (2002)

    Google Scholar 

  33. Schäfer, J., Poetzsch-Heffter, A.: Simple fuzzy ownership domains (unpublished) (Preliminary version), Available at: http://softech.informatik.uni-kl.de/~janschaefer

  34. Sun Microsystems, Inc., Palo Alto, CA. Java CardTM2.1.1 Virtual Machine Specification (May 2000)

    Google Scholar 

  35. Sun Microsystems, Inc. JavaTM2 Platform, Standard Edition, v 1.4.2 API Specification (2003), http://java.sun.com/j2se/1.4.2/docs/api/

  36. Szyperski, C., Gruntz, D., Murer, S.: Component Software — Beyond Object-Oriented Programming, 2nd edn. Addison-Wesley, Reading (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Kaiserslautern, Germany

    Arnd Poetzsch-Heffter & Jan Schäfer

Authors
  1. Arnd Poetzsch-Heffter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan Schäfer
    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

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Poetzsch-Heffter, A., Schäfer, J. (2006). Modular Specification of Encapsulated Object-Oriented Components. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2005. Lecture Notes in Computer Science, vol 4111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11804192_15

Download citation

  • DOI: https://doi.org/10.1007/11804192_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36749-9

  • Online ISBN: 978-3-540-36750-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation