Featherweight Java

ACM Transactions on Programming Languages and Systems - Tập 23 Số 3 - Trang 396-450 - 2001
Atsushi Igarashi1, Benjamin C. Pierce2, Philip Wadler3
1University of Tokyo, Tokyo, Japan
2University of Pennsylvania, Philadelphia, PA
3Avaya Labs, Basking Ridge, NJ

Tóm tắt

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 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 minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying 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 give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

Từ khóa


Tài liệu tham khảo

ABADI , M. AND CARDELLI , L. 1996. A Theory of Objects . Springer Verlag , New York, NY .]] ABADI,M.AND CARDELLI, L. 1996. A Theory of Objects. Springer Verlag, New York, NY.]]

AGESEN , O. , FREUND , S.N. , AND MITCHELL , J. C. 1997 . Adding type parameterization to the Java language . In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'97) . SIGPLAN Not. 32, 10. ACM Press, Atlanta, GA , 49 - 65 .]] 10.1145/263698.263720 AGESEN, O., FREUND,S.N.,AND MITCHELL, J. C. 1997. Adding type parameterization to the Java language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'97). SIGPLAN Not. 32, 10. ACM Press, Atlanta, GA, 49-65.]] 10.1145/263698.263720

ANCONA , D. AND ZUCCA , E. 2001 . True modules for Java-like languages . In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP2001) , J. L. Knudsen, Ed. Lecture Notes in Computer Science. Springer-Verlag, Budapest, Hungary.]] ANCONA,D.AND ZUCCA, E. 2001. True modules for Java-like languages. In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP2001), J. L. Knudsen, Ed. Lecture Notes in Computer Science. Springer-Verlag, Budapest, Hungary.]]

BARENDREGT , H. P. 1984. The Lambda Calculus, revised ed. North Holland , Amsterdam, The Netherlands .]] BARENDREGT, H. P. 1984. The Lambda Calculus, revised ed. North Holland, Amsterdam, The Netherlands.]]

BONO , V. AND FISHER , K. 1998 . An imperative first-order calculus with object extension . In Proceedings of the 12th European Conference on Object-Oriented Programming (ECOOP'98) , E. Jul, Ed. LNCS 1445. Springer Verlag , 462 - 497 .]] BONO,V.AND FISHER, K. 1998. An imperative first-order calculus with object extension. In Proceedings of the 12th European Conference on Object-Oriented Programming (ECOOP'98), E. Jul, Ed. LNCS 1445. Springer Verlag, 462-497.]]

BONO , V. , PATEL , A.J. , AND SHMATIKOV , V. 1999 a. A core calculus of classes and mixins . In Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99) . LNCS 1628. Springer Verlag , 43 - 66 .]] BONO, V., PATEL,A.J.,AND SHMATIKOV, V. 1999a. A core calculus of classes and mixins. In Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99). LNCS 1628. Springer Verlag, 43-66.]]

BONO , V. , PATEL , A.J. , SHMATIKOV , V. , AND MITCHELL , J. C. 1999 b. A core calculus of classes and objects . In Proceedings of the 15th Conference on the Mathematical Foundations of Programming Semantics (MFPS XV). Elsevier. Available through http://www.elsevier.nl/locate/entcs/ volume 20 .html.]] BONO, V., PATEL,A.J.,SHMATIKOV,V.,AND MITCHELL, J. C. 1999b. A core calculus of classes and objects. In Proceedings of the 15th Conference on the Mathematical Foundations of Programming Semantics (MFPS XV). Elsevier. Available through http://www.elsevier.nl/locate/entcs/ volume20.html.]]

BRACHA , G. , ODERSKY , M. , STOUTAMIRE , D. , AND WADLER , P. 1998 . Making the future safe for the past: Adding genericity to the Java programming language . In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98) , C. Chambers, Ed. ACM Press, New York, NY , 183 - 200 .]] 10.1145/286936.286957 BRACHA, G., ODERSKY, M., STOUTAMIRE,D.,AND WADLER, P. 1998. Making the future safe for the past: Adding genericity to the Java programming language. In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98), C. Chambers, Ed. ACM Press, New York, NY, 183-200.]] 10.1145/286936.286957

BRUCE , K. B. 1994 . A paradigmatic object-oriented programming language: Design, static typing and semantics . J. Funct. Program. 4 , 2 (April), 127-206.]] BRUCE, K. B. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. J. Funct. Program. 4, 2 (April), 127-206.]]

10.1006/inco.1994.1013

CARTWRIGHT , R. AND STEELE JR., G. L. 1998. Compatible genericity with run-time types for the Java programming language . In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98) , C. Chambers, Ed. ACM Press, New York, NY , 201 - 215 .]] 10.1145/286936.286958 CARTWRIGHT,R.AND STEELE JR., G. L. 1998. Compatible genericity with run-time types for the Java programming language. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'98), C. Chambers, Ed. ACM Press, New York, NY, 201-215.]] 10.1145/286936.286958

10.1002/(SICI)1096-9942(199901/03)5:1%3C3::AID-TAPO2%3E3.0.CO;2-T

DUGGAN , D. 1999 . Modular type-based reverse engineering of parameterized types in Java code . In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99) , L. M. Northrop, Ed. ACM Press, New York, NY , 97 - 113 .]] 10.1145/320384.320393 DUGGAN, D. 1999. Modular type-based reverse engineering of parameterized types in Java code. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), L. M. Northrop, Ed. ACM Press, New York, NY, 97-113.]] 10.1145/320384.320393

FELLEISEN M.AND FRIEDMAN D. P. 1998. A Little Java A Few Patterns. MIT Press Cambridge MA.]] FELLEISEN M.AND FRIEDMAN D. P. 1998. A Little Java A Few Patterns. MIT Press Cambridge MA.]]

10.1002/(SICI)1096-9942(1998)4:1%3C3::AID-TAPO2%3E3.3.CO;2-2

FLATT , M. , KRISHNAMURTHI , S. , AND FELLEISEN , M. 1998 a . Classes and mixins . In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press , New York, NY , 171 - 183 .]] 10.1145/268946.268961 FLATT, M., KRISHNAMURTHI,S.,AND FELLEISEN, M. 1998a . Classes and mixins. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 171-183.]] 10.1145/268946.268961

IGARASHI , A. AND PIERCE , B. C. 2000 . On inner classes . In Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000) , E. Bertino, Ed. LNCS 1850. Springer Verlag, 129 - 153 . Extended version to appear in Inf. Comput.]] IGARASHI,A.AND PIERCE, B. C. 2000. On inner classes. In Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000), E. Bertino, Ed. LNCS 1850. Springer Verlag, 129-153. Extended version to appear in Inf. Comput.]]

IGARASHI , A. , PIERCE , B.C. , AND WADLER , P. 2001 . A recipe for raw types . In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8) . London, UK. Available through http://www.cs.williams.edu/kim/FOOL/FOOL8.html.]] IGARASHI, A., PIERCE,B.C.,AND WADLER, P. 2001. A recipe for raw types. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8). London, UK. Available through http://www.cs.williams.edu/kim/FOOL/FOOL8.html.]]

LEAGUE , C. , TRIFONOV , V. , AND SHAO , Z. 2001 . Type-preserving compilation of Featherweight Java . In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8) . London, UK. Available through http://www.cs.williams.edu/kim/FOOL/ FOOL8.html.]] LEAGUE, C., TRIFONOV,V.,AND SHAO, Z. 2001. Type-preserving compilation of Featherweight Java. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8). London, UK. Available through http://www.cs.williams.edu/kim/FOOL/ FOOL8.html.]]

MYERS , A.C. , BANK , J.A. , AND LISKOV , B. 1997 . Parameterized types for Java . In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press , New York, NY , 132 - 145 .]] 10.1145/263699.263714 MYERS,A.C.,BANK,J.A.,AND LISKOV, B. 1997. Parameterized types for Java. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 132-145.]] 10.1145/263699.263714

NIPKOW , T. AND VON OHEIMB, D. 1998. Java light is type-safe- definitely . In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press , New York, NY , 161 - 170 .]] 10.1145/268946.268960 NIPKOW,T.AND VON OHEIMB, D. 1998. Java light is type-safe- definitely. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 161-170.]] 10.1145/268946.268960

ODERSKY , M. AND WADLER , P. 1997 . Pizza into Java: Translating theory into practice . In Proceedings of the ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press , New York, NY , 146 - 159 .]] 10.1145/263699.263715 ODERSKY,M.AND WADLER, P. 1997. Pizza into Java: Translating theory into practice. In Proceedings of the ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, New York, NY, 146-159.]] 10.1145/263699.263715

PIERCE , B. C. 2002. Types and Programming Languages . MIT Press , Cambridge, MA .]] PIERCE, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA.]]

PIERCE , B.C. AND TURNER , D. N. 1994 . Simple type-theoretic foundations for object-oriented programming . J. Funct. Program. 4 , 2 (April), 207-247.]] PIERCE,B.C.AND TURNER, D. N. 1994. Simple type-theoretic foundations for object-oriented programming. J. Funct. Program. 4, 2 (April), 207-247.]]

SCHULTZ , U. 2001 . Partial evaluation for class-based object-oriented languages . In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO II), O. Danvy and A. Filinski, Eds. LNCS 2053. Springer Verlag , 173 - 197 .]] SCHULTZ, U. 2001. Partial evaluation for class-based object-oriented languages. In Proceedings of the 2nd Symposium on Programs as Data Objects (PADO II), O. Danvy and A. Filinski, Eds. LNCS 2053. Springer Verlag, 173-197.]]

STUDER T. 2000. Constructive foundations for Featherweight Java. Available through http:// iamwww.unibe.ch/tstuder/.]] STUDER T. 2000. Constructive foundations for Featherweight Java. Available through http:// iamwww.unibe.ch/tstuder/.]]

VIROLI , M. AND NATALI , A. 2000 . Parametric polymorphism in Java: an approach to translation based on reflective features . In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00) , D. Lea, Ed. ACM Press, New York, NY , 146 - 165 .]] 10.1145/353171.353182 VIROLI,M.AND NATALI, A. 2000. Parametric polymorphism in Java: an approach to translation based on reflective features. In Proceedings of the ACMSIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), D. Lea, Ed. ACM Press, New York, NY, 146-165.]] 10.1145/353171.353182

10.1006/inco.1994.1093

Thông tin
Thông tin xuất bản

ACM Transactions on Programming Languages and Systems

Tập 23 Số 3

396-450

Thông tin tác giả