Object and reference immutability using Java generics

ABSTRACT

A compiler-checked immutability guarantee provides useful documentation, facilitates reasoning, and enables optimizations. This paper presents Immutability Generic Java (IGJ), a novel language extension that expresses immutability without changing Java's syntax by building upon Java's generics and annotation mechanisms. In IGJ, each class has one additional type parameter that is Immutable, Mutable, or ReadOnly. IGJ guarantees both reference immutability (only mutable references can mutate an object) and object immutability (an immutable reference points to an immutable object). IGJ is the first proposal for enforcing object immutability within Java's syntax and type system, and its reference immutability is more expressive than previous work. IGJ also permits covariant changes of type parameters in a type-safe manner, e.g., a readonly list of integers is a subtype of a readonly list of numbers. IGJ extends Java's type system with a few simple rules. We formalize this type system and prove it sound. Our IGJ compiler works by type-erasure and generates byte-code that can be executed on any JVM without runtime penalty.

REFERENCES

• 1: S. Artzi, M. D. Ernst, A. Kiežun, C. Pacheco, and J. H. Perkins. Finding the needles in the haystack: Generating legal test inputs for object-oriented programs. In M-TOOS, Oct. 2006.
• 2: Adrian Birka , Michael D. Ernst, A practical type system and language for reference immutability, Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 24-28, 2004, Vancouver, BC, Canada
• 3: Chandrasekhar Boyapati , Martin C. Rinard, Safejava: a unified type system for safe programming, Massachusetts Institute of Technology, 2004
• 4: J. Boyland. Why we should not add readonly to Java (yet). In FTfJP, July 2005.
• 5: John Boyland , James Noble , William Retert, Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only, Proceedings of the 15th European Conference on Object-Oriented Programming, p.2-27, June 18-22, 2001
• 6: Gilad Bracha , Martin Odersky , David Stoutamire , Philip Wadler, Making the future safe for the past: adding genericity to the Java programming language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.183-200, October 18-22, 1998, Vancouver, British Columbia, Canada
• 7: Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
• 8: Dave Clarke , Sophia Drossopoulou, Ownership, encapsulation and the disjointness of type and effect, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 9: L. R. Clausen. A Java bytecode optimizer using side-effect analysis. Concurrency: Practice and Experience, 9(11):1031--1045, 1997.
• 10: Valentin Dallmeier , Christian Lindig , Andrzej Wasylkowski , Andreas Zeller, Mining object behavior with ADABU, Proceedings of the 2006 international workshop on Dynamic systems analysis, May 23-23, 2006, Shanghai, China [doi>10.1145/1138912.1138918]
• 11: R. DeLine and M. Fähndrich. Typestates for objects. In ECOOP, pages 465--490, June 2004.
• 12: W. Dietl and P. Müller. Universes: Lightweight ownership for JML. Journal of Object Technology (JOT), 4(8):5--32, Oct. 2005.
• 13: J. J. Dolado , M. Harman , M. C. Otero , L. Hu, An Empirical Investigation of the Influence of a Type of Side Effects on Program Comprehension, IEEE Transactions on Software Engineering, v.29 n.7, p.665-670, July 2003 [doi>10.1109/TSE.2003.1214329]
• 14: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 15: M. D. Ernst and D. Coward. JSR 308: Annotations on Java types. http://pag.csail.mit.edu/jsr308/, Oct. 17, 2006.
• 16: Manuel Fähndrich , K. Rustan M. Leino, Declaring and checking non-null types in an object-oriented language, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 17: M. Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 2000.
• 18: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 19: Shan Shan Huang , David Zook , Yannis Smaragdakis, cJ: enhancing java with safe type conditions, Proceedings of the 6th international conference on Aspect-oriented software development, March 12-16, 2007, Vancouver, British Columbia, Canada [doi>10.1145/1218563.1218584]
• 20: Atsushi Igarashi , Benjamin C. Pierce , Philip Wadler, Featherweight Java: a minimal core calculus for Java and GJ, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.396-450, May 2001 [doi>10.1145/503502.503505]
• 21: Atsushi Igarashi , Mirko Viroli, Variant parametric types: A flexible subtyping scheme for generics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.5, p.795-847, September 2006 [doi>10.1145/1152649.1152650]
• 22: Günter Kniesel , Dirk Theisen, JAC—access right based encapsulation for Java, Software—Practice & Experience, v.31 n.6, p.555-576, May 2001 [doi>10.1002/spe.372]
• 23: Y. Lu and J. Potter. On ownership and accessibility. In ECOOP, pages 99--123, July 2006.
• 24: Behavior Capture and Test: Automated Analysis of Component Integration, Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, p.292-301, June 16-20, 2005 [doi>10.1109/ICECCS.2005.25]
• 25: Igor Pechtchanski , Vivek Sarkar, Immutability specification and its applications, Proceedings of the 2002 joint ACM-ISCOPE conference on Java Grande, p.202-211, November 03-05, 2002, Seattle, Washington, USA [doi>10.1145/583810.583833]
• 26: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 27: Alex Potanin , James Noble , Dave Clarke , Robert Biddle, Generic ownership for generic Java, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 28: A. Sǎlcianu. Pointer analysis for Java programs: Novel techniques and applications. PhD thesis, MIT Dept. of EECS, Sept. 2006.
• 29: M. Skoglund and T. Wrigstad. A mode system for read-only references in Java. In FTfJP, June 2001.
• 30: Oksana Tkachuk , Matthew B. Dwyer, Adapting side effects analysis for modular program model checking, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 31: Matthew S. Tschantz , Michael D. Ernst, Javari: adding reference immutability to Java, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 32: T. Xie. Augmenting automatically generated unit-test suites with regression oracle checking. In ECOOP, pages 380--403, July 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

General Terms:
Design, Languages, Theory

Keywords:
IGJ, const, generic, immutability, java, readonly