Skip to main content

A Model for Java with Wildcards

  • Conference paper

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

Abstract

Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.

This is a preview of subscription content, log in via an institution.

Buying options

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

Learn about 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)

    Google Scholar 

  2. Barendregt, H.: The Lambda Calculus. Revised edn. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

  3. Bracha, G.: Generics in the Java programming language (2004), http://java.sun.com/j2se/1.5/pdf/generics-tutorial.pdf

  4. Cameron, N., Drossopoulou, S., Noble, J., Smith, M.: Multiple Ownership. In: OOPSLA 2007 (October 2007)

    Google Scholar 

  5. Cameron, N., Ernst, E., Drossopoulou, S.: Towards an existential types model for java wildcards. In: 9th Workshop on Formal Techniques for Java-like Programs (2007)

    Google Scholar 

  6. Cardelli, L., Leroy, X.: Abstract types and the dot notation. Research report 56, DEC Systems Research Center (1990)

    Google Scholar 

  7. Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Computing Surveys 17(4), 471–522 (1985)

    Article  Google Scholar 

  8. Chin, W.-N., Craciun, F., Khoo, S.-C., Popeea, C.: A flow-based approach for variant parametric types. In: Proceedings of the 2006 ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA 2006). ACM Press, New York (2006)

    Google Scholar 

  9. Clarke, D., Drossopoulou, S., Noble, J., Wrigstad, T.: Tribe: a simple virtual class calculus. In: AOSD 2007: Proceedings of the 6th international conference on Aspect-oriented software development, Vancouver, British Columbia, Canada, pp. 121–134. ACM, New York (2007), http://doi.acm.org/10.1145/1218563.1218578

    Chapter  Google Scholar 

  10. Ghelli, G., Pierce, B.: Bounded existentials and minimal typing. Theoretical Computer Science 193(1-2), 75–96 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  11. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification Third Edition. Addison-Wesley, Boston (2005)

    Google Scholar 

  12. Grossman, D.: Existential types for imperative languages. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 21–35. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001); An earlier version of this work appeared at OOPSLA 1999.

    Article  Google Scholar 

  14. Igarashi, A., Viroli, M.: Variant parametric types: A flexible subtyping scheme for generics. ACM Trans. Program. Lang. Syst. 28(5), 795–847 (2006); An earlier version appeared as On variance-based subtyping for parametric types at (ECOOP 2002)

    Google Scholar 

  15. Kennedy, A.J., Pierce, B.C.: On decidability of nominal subtyping with variance. In: International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD 2007), Nice, France (January 2007)

    Google Scholar 

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

  17. Torgersen, M., Ernst, E., Hansen, C.P.: Wild FJ. In: 12th International Workshop on Foundations of Object-Oriented Languages (FOOL 12), Long Beach, California, ACM Press, New York (2005)

    Google Scholar 

  18. Madsen, O.L., Moller-Pedersen, B.: Virtual classes: a powerful mechanism in object-oriented programming. In: OOPSLA 1989: Conference proceedings on Object-oriented programming systems, languages and applications, pp. 397–406. ACM Press, New York (1989)

    Chapter  Google Scholar 

  19. Mazurak, K., Zdancewic, S.: Note on Type Inference for Java 5: Wildcards, F-Bounds, and Undecidability (2006), http://www.cis.upenn.edu/~stevez/note.html

  20. Mitchell, J.C., Plotkin, G.D.: Abstract types have existential types. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 37–51. ACM Press, New York (1985)

    Chapter  Google Scholar 

  21. Pierce, B.C.: Bounded quantification is undecidable. In: POPL 1992: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 305–315. ACM Press, New York (1992)

    Chapter  Google Scholar 

  22. Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)

    Google Scholar 

  23. Krab Thorup, K., Torgersen, M.: Unifying genericity - combining the benefits of virtual types and parameterized classes. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 186–204. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Torgersen, M., Hansen, C.P., Ernst, E., von der Ahé, P., Bracha, G., Gafter, N.: Adding wildcards to the Java programming language. Journal of Object Technology 3(11), 97–116 (2004); Special issue: OOPS track at SAC 2004, Nicosia/Cyprus.

    Google Scholar 

  25. Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 35–50. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Viroli, M., Rimassa, G.: On access restriction with Java wildcards. Journal of Object Technology 4(10), 117–139 (2005); Special issue: OOPS track at SAC 2005, Santa Fe/New Mexico. The earlier version in the proceedings of SAC 2005 appeared as Understanding access restriction of variant parametric types and Java wildcards.

    Google Scholar 

  27. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  28. Wrigstad, T., Clarke, D.: Existential owners for ownership types. JOT 6(4), 141–159 (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Jan Vitek

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cameron, N., Drossopoulou, S., Ernst, E. (2008). A Model for Java with Wildcards. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70592-5_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70591-8

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics