Object and reference immutability using Java generics

Download: PDF, slides (PDF), slides (PowerPoint), IGJ implementation.

“Object and reference immutability using Java generics” by Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kieżun, and Michael D. Ernst. In ESEC/FSE 2007: Proceedings of the 11th European Software Engineering Conference and the 15th ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Dubrovnik, Croatia), Sep. 2007, pp. 75-84.
A tool demonstration appeared as “Enforcing reference and object immutability in Java” by Mahmood Ali, Yoav Zibin, Matthew M. Papi, and Michael D. Ernst. In OOPSLA Companion: Object-Oriented Programming Systems, Languages, and Applications, (Nashville, TN, USA), Oct. 2008, pp. 725-726.
A previous version appeared as “Object and reference immutability using Java generics” by Yoav Zibin, Alex Potanin, Shay Artzi, Adam Kieżun, and Michael D. Ernst. MIT Computer Science and Artificial Intelligence Laboratory technical report MIT-CSAIL-TR-2007-018, (Cambridge, MA), March 16, 2007.

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 Mutable, Immutable, 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.

Download: PDF, slides (PDF), slides (PowerPoint), IGJ implementation.

BibTeX entry:

@inproceedings{ZibinPAAKE2007,
   author = {Yoav Zibin and Alex Potanin and Mahmood Ali and Shay Artzi
	and Adam Kie{\.z}un and Michael D. Ernst},
   title = {Object and reference immutability using {Java} generics},
   booktitle = {ESEC/FSE 2007: Proceedings of the 11th European Software
	Engineering Conference and the 15th {ACM} {SIGSOFT} Symposium on
	the Foundations of Software Engineering},
   pages = {75--84},
   address = {Dubrovnik, Croatia},
   month = sep,
   year = {2007}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.