Abstract
This paper presents Welterweight Java (WJ), a new minimal core Java calculus intended to be a suitable starting point for investigations in the semantics of Java-like programs. To this end, WJ adds a few extra pounds to Featherweight Java. WJ is imperative and stateful, which is a frequent extension of Featherweight Java. To account for the importance of concurrency, WJ models Java’s thread-based concurrency and lock-based synchronisation. The design of WJ is distilled from recent work on concurrent Java-like systems. We believe that the calculus is a good starting point for extensions. We illustrate the potential of the calculus by showing two extensions. The first is a version of WJ extended with deep ownership. This serves two purposes—it is a minimal formalisation of ownership, interesting in its own right, and shows how easily WJ can be extended. The second is a simple non-null types system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahern, A., Yoshida, N.: Formalising Java RMI with Explicit Code Mobility. In: Proceedings of OOPSLA, pp. 403–422 (2005)
Bierman, G.M., Parkinson, M.J., Pitts, A.M.: MJ: An imperative core calculus for Java and Java with effects. Technical report, University of Cambridge (2003)
Clarke, D., Wrigstad, T.: External Uniqueness is Unique Enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 59–67. Springer, Heidelberg (2003)
Clarke, D.: Object Ownership and Containment. PhD thesis, School of Computer Science and Engineering, University of New South Wales, Sydney, Australia (2001)
Clarke, D., Drossopolou, S.: Ownership, encapsulation and the disjointness of type and effect. In: Proceedings of OOPSLA (November 2002)
Clifton, C., Leavens, G.T.: MiniMAO1: Investigating the semantics of proceed. Science of Computer Programming 63(3), 321–374 (2006)
Cunningham, D., Drossopoulou, S., Eisenbach, S.: Universes for race safety. In: VAMP ’07, September 2007, pp. 20–51 (2007)
Dietl, W., Drossopoulou, S., Müller, P.: Generic universe types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 28–53. Springer, Heidelberg (2007)
Dietl, W., Müller, P.: Universes: Lightweight Ownership for JML. Journal of Object Technology 4(8), 5–32 (2002)
Fähndrich, M., Rustan, K., Leino, M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of OOPSLA, pp. 302–312. ACM, New York (2003)
Fähndrich, M., Xia, S.: Establishing object invariants with delayed types. SIGPLAN Not. 42(10), 337–350 (2007)
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, p. 241. Springer, Heidelberg (1999)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM TOPLAS 23(3), 396–450 (2001)
Malayeri, D., Aldrich, J.: Cz: multiple inheritance without diamonds. In: Proceedings of OOPSLA, pp. 21–40. ACM, New York (2009)
Östlund, J., Wrigstad, T.: Welterweight Java website (2009), http://user.it.uu.se/~johos902
Östlund, J., Wrigstad, T., Clarke, D., Åkerblom, B.: Ownership, Uniqueness, and Immutability. In: Objects, Components, Models and Patterns (Proceedings of 46th International Conference on Objects, Models, Components, Patterns). Lecture Notes in Business Information Processing, vol. 11, pp. 178–197. Springer, Heidelberg (2008)
Parkinson, M., Strniša, R.: Lightweight Java web pages (2008–2009), http://www.cl.cam.ac.uk/research/pls/javasem/lj/
Qi, X., Myers, A.C.: Masked types for sound object initialization. SIGPLAN Not. 44(1), 53–65 (2009)
Sewell, P., Nardelli, F.Z.: Ott Website (2010), http://www.cl.cam.ac.uk/~pes20/ott/
van Dooren, M., Joosen, W.: A modular type system for first-class composition inheritance. Technical Report Report CW 534, Department of Computer Science, K.U.Leuven (January 2009)
Vaziri, M., Tip, F., Dolby, J., Hammer, C., Vitek, J.: A type system for data-centric synchronization. To appear at ECOOP 2010 (2010)
Wrigstad, T., Clarke, D.: Existential owners for ownership types. Journal of Object Technology 6(4) (May/June 2007)
Wrigstad, T., Pizlo, F., Meawad, F., Zhao, L., Vitek, J.: Loci: Simple thread-locality for java. In: Drossopoulou, S. (ed.) ECOOP 2009 – Object-Oriented Programming. LNCS, vol. 5653, pp. 445–469. Springer, Heidelberg (2009)
Wrigstad, T., Nardelli, F.Z., Lebresne, S., Östlund, J., Vitek, J.: Integrating typed and untyped code in a scripting language. In: POPL ’10, pp. 377–388. ACM, New York (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Östlund, J., Wrigstad, T. (2010). Welterweight Java. In: Vitek, J. (eds) Objects, Models, Components, Patterns. TOOLS 2010. Lecture Notes in Computer Science, vol 6141. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13953-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-13953-6_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13952-9
Online ISBN: 978-3-642-13953-6
eBook Packages: Computer ScienceComputer Science (R0)