Full Abstraction at Package Boundaries of Object-Oriented Languages

  • Yannick Welsch
  • Arnd Poetzsch-Heffter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


We develop a fully abstract trace-based semantics for sets of classes in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the package and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap, support class hiding, and provide fully abstract package denotations. The soundness and completeness of our approach is proven using innovative simulation techniques.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 11–41. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Ábrahám, E., Bonsangue, M.M., de Boer, F.S., Steffen, M.: Object connectivity and full abstraction for a concurrent calculus of classes. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 37–51. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Back, R.J.J., Akademi, A., Wright, J.V.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)CrossRefzbMATHGoogle Scholar
  4. 4.
    Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM 52(6), 894–960 (2005)CrossRefzbMATHGoogle Scholar
  5. 5.
    Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. The Java Series. Addison-Wesley, Boston (2005)zbMATHGoogle Scholar
  6. 6.
    Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating objects with confined types. In: OOPSLA, pp. 241–253 (2001)Google Scholar
  7. 7.
    Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  8. 8.
    Jeffrey, A., Rathke, J.: Java Jr.: Fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Koutavas, V., Wand, M.: Bisimulations for untyped imperative objects. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 146–161. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Koutavas, V., Wand, M.: Reasoning about class behavior. In: Informal Workshop Record of FOOL 2007 (January 2007)Google Scholar
  11. 11.
    Milner, R.: Fully abstract models of typed lambda-calculi. Theor. Comput. Sci. 4(1), 1–22 (1977)CrossRefzbMATHGoogle Scholar
  12. 12.
    Morris, J.H.: Lambda-calculus models of programming languages. Tech. Rep. 57, MIT Laboratory for Computer Science (1968)Google Scholar
  13. 13.
    Plotkin, G.D.: Lcf considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977)CrossRefzbMATHGoogle Scholar
  14. 14.
    Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  15. 15.
    Silva, L., Naumann, D.A., Sampaio, A.: Refactoring and representation independence for class hierarchies: Extended abstract. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, pp. 8:1–8:7. ACM, New York (2010)Google Scholar
  16. 16.
    Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. Theoretical Computer Science 375 (2007)Google Scholar
  17. 17.
    Sumii, E., Pierce, B.C.: A bisimulation for type abstraction and recursion. Journal of the ACM 54 (2007)Google Scholar
  18. 18.
    Welsch, Y., Poetzsch-Heffter, A.: Full abstraction at package boundaries of object-oriented languages. Tech. Rep. 384/11 (May 2011),
  19. 19.
    Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Yannick Welsch
    • 1
  • Arnd Poetzsch-Heffter
    • 1
  1. 1.University of KaiserslauternGermany

Personalised recommendations