Featherwieght Java: a minimal core calculus for Java and GJ

ABSTRACT

Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.Featherweight Java bears a similar relation to full Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational “feel,” providing classes, methods, fields, inheritance, and dynamic typecasts, with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The syntax, type rules, and operational semantics of Featherweight Java fit on one page, making it easier to understand the consequences of extensions and variations.As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and sketch a proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Ole Agesen , Stephen N. Freund , John C. Mitchell, Adding type parameterization to the Java language, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.49-65, October 05-09, 1997, Atlanta, Georgia, United States
• 3: H. P. Barendregt. The Lambda Calculus. North Holland, revised edition, 1984.
• 4: Viviana Bono , Kathleen Fisher, An Imperative, First-Order Calculus with Object Extension, Proceedings of the 12th European Conference on Object-Oriented Programming, p.462-497, July 20-24, 1998
• 5: Viviana Bono , Amit Patel , Vitaly Shmatikov, A Core Calculus of Classes and Mixins, Proceedings of the 13th European Conference on Object-Oriented Programming, p.43-66, June 14-18, 1999
• 6: Viviana Bono, Amit J. Patel, Vitaly Shmatikov, and John C. Mitchell. A core calculus of classes and objects. In Fifteenth Confertence on the Mathematical Foundations of Programming Semantics, April 1999.
• 7: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, ACM SIGPLAN Notices, v.33 n.10, p.183-200, Oct. 1998
• 8: Kim B. Bruce. A paradigmatic object-oriented programming language' Design, static typing and semantics. Journal of Functional Programming, 4(2), April 1994. Preliminary version in POPL 1993, under the title "Safe type checking in a statically typed object-oriented programming language".
• 9: Luca Cardelli , Simone Martini , John C. Mitchell , Andre Scedrov, An extension of system F with subtyping, Information and Computation, v.109 n.1-2, p.4-56, Feb. 15/March 1994 [doi>10.1006/inco.1994.1013]
• 10: Robert Cartwright , Guy L. Steele, Jr., Compatible genericity with run-time types for the Java programming language, ACM SIGPLAN Notices, v.33 n.10, p.201-215, Oct. 1998
• 11: Sophia Drossopoulou , Susan Eisenbach , Sarfraz Khurshid, Is the Java type system sound?, Theory and Practice of Object Systems, v.5 n.1, p.3-24, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<3::AID-TAPO2>3.0.CO;2-T]
• 12: Matthias Felleisen , Daniel P. Friedman, A little Java, a few patterns, Massachusetts Institute of Technology, Cambridge, MA, 1998
• 13: Kathleen Fisher , John C. Mitchell, On the relationship between classes, objects, and data abstraction, Theory and Practice of Object Systems, v.4 n.1, p.3-25, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<3::AID-TAPO2>3.3.CO;2-2]
• 14: Matthew Flatt , Shriram Krishnamurthi , Matthias Felleisen, Classes and mixins, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268961]
• 15: Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. A programmer's reduction semantics for classes and mixins. Technical Report TR97-293, Computer Science Department, Rice University, February 1998. Corrected version appeared in June, 1999.
• 16: Atsushi Igarashi and Benjamin C. Pierce. On inner classes, july 1999. Submitted for publication.
• 17: Joseph A. Bank , Andrew C. Myers , Barbara Liskov, Parameterized types for Java, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.132-145, January 15-17, 1997, Paris, France [doi>10.1145/263699.263714]
• 18: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 19: Martin Odersky , Philip Wadler, Pizza into Java: translating theory into practice, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-159, January 15-17, 1997, Paris, France [doi>10.1145/263699.263715]
• 20: Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994. Preliminary version in Principles of Programming Languages (POPL), 1993.
• 21: Don Syme. Proving Java type soundness. Technical Report 427, Computer Laboratory, University of Cambridge, June 1997.
• 22: Mitchell Wand, Type inference for objects with instance variables and inheritance, Theoretical aspects of object-oriented programming: types, semantics, and language design, MIT Press, Cambridge, MA, 1994

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Java

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Design, Languages, Performance, Theory, Verification

Keywords:
implementation, language design, theoretical foundations