Abstracts - 2007
Object and Reference Immutability Using Java Generics
Yoav Zibin, Alex Potanin, Shay Artzi, Adam Kiezun & Michael D. Ernst
Immutability information is useful in many software engineering tasks, such as modeling , verification , compile- and runtime optimizations , refactoring , test input generation , regression oracle creation , invariant detection , specification mining , and program comprehension . Three important varieties of immutability guarantee are immutable classes, object immutability, and reference immutability.
No instance of an immutable class may be changed; examples in Java include String and all subclasses of Number including Integer and BigDecimal. Java's type system has no way of expressing or checking this property.
Object immutability guarantees that an object cannot be modified, even if other instances of the same class can be. For example, some instances of List in a given program may be immutable, whereas others can be modified. Object immutability gives strong guarantees that can be used for pointer analysis and optimizations, such as sharing between threads without synchronization.
Reference immutability [7, 8, 9, 11] guarantees that a given reference cannot be used to modify its referent. Such a system supports readonly references that have no mutating privileges, and mutable references that point to a mutable object and can call mutating methods. Reference immutability is required in order to specify interfaces, such as that a procedure may not modify its arguments (even if the caller retains the right to do so) or a client cannot modify values returned from a module. However, past work does not guarantee object immutability, unless the reference immutability is combined with an alias/escape analysis to guarantee that no aliases to an object exist.
Immutability Generic Java (IGJ)
This work develops a language extension of Java called Immutability
Generic Java (IGJ) that supports both object immutability (an immutable
reference points to an immutable object) and reference immutability (only
mutable references can mutate an object). Each object is either mutable
or immutable, and each reference is Immutable, Mutable, or ReadOnly. Inspired
by work that combines ownership and generics , the distinctions are
expressed without changing Java’s syntax by adding one new generic parameter
(at the beginning of the list of generic parameters):
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 generic arguments 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 generates byte-code that can be executed on any JVM without runtime penalty.
IGJ is designed to satisfy the following design principles:
The following presents two IGJ classes:
 S. Artzi, M. D. Ernst, A. Kiezun, C. Pacheco, and J. H. Perkins. Finding the needles in the haystack: Generating legal test inputs for object-oriented programs. Technical Report MIT-CSAIL-TR-2006- 056, MIT CSAIL, Sept. 5, 2006.
 L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. STTT, 7(3):212–232, June 2005.
 V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller. Mining object behavior with ADABU. In WODA, pages 17–24, May 2006.
 M. D. Ernst, J. Cockrell,W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):99–123, Feb. 2001.
 M. Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 2000.
 Jose Javier Dolado and Mark Harman and Mari Carmen Otero and Lin Hu. An empirical investigation of the influence of a type of side effects on program comprehension. IEEE TSE, 29(7):665–670, July 2003.
 I. Pechtchanski and V. Sarkar. Immutability specification and its applications. In Java Grande, pages 202–211, Nov. 2002.
 A. Potanin, J. Noble, D. Clarke, and R. Biddle. Generic ownership for generic Java. In OOPSLA, pages 311–324, Oct. 2006.
 M. Skoglund and T. Wrigstad. A mode system for read-only references in Java. In 3rd Workshop on Formal Techniques for Java Programs, June 18, 2001. Revised.
 O. Tkachuk and M. B. Dwyer. Adapting side effects analysis for modular program model checking. In ESEC/FSE, pages 188–197, Sept. 2003.
 M. S. Tschantz and M. D. Ernst. Javari: Adding reference immutability to Java. In OOPSLA, pages 211–230, Oct. 2005.
 T. Xie. Augmenting automatically generated unit-test suites with regression oracle checking. In ECOOP, pages 380–403, July 2006.