Transcript JavaGenerics_presented

Object and Reference
Immutability using Java Generics
Yoav Zibin(1), Alex Potanin(2), Shay Artzi(1),
Adam Kiezun(1), and Michael D. Ernst(1)
1) MIT Computer Science and Artificial Intelligence Lab, USA
2) Victoria University of Wellington, New-Zealand
Presenting: Ori Arad ([email protected]) – 14/2/07
Immutability – What for?...




Program
comprehension
Verification
Compile & Run-time
optimizations
Invariant detection





Refactoring
Test input
generation
Regression oracle
creation
Specification mining
Modeling
2/23
Immutability varieties

Class immutability


Object immutability


No instance of an immutable class may be
change after creation (e.g. String, Integer etc.)
Immutable instances may not be changed, while
other instances (of the same class) may…
Reference immutability

a given reference cannot be used to modify its
referent.
3/23
IGJ - Immutability Generic Java

Object immutability:


Reference immutability:


An object: mutable or immutable.
A reference: Immutable, Mutable, or
ReadOnly
Class immutability

Also support Class immutability
4/23
IGJ - Immutability Generic Java
1: // An immutable reference to an immutable date; side effects are prohibited
2: Date<Immutable> immutD = new Date<Immutable>();
3: // A mutable reference to a mutable date; side effects are permitted
4: Date<Mutable> mutD = new Date<Mutable>();
5: // A readonly reference to any date; side effects are prohibited
6: Date<ReadOnly> roD = ... ? immutD : mutD;
one new generic parameter (at the beginning
of the list of generic parameters) was added
5/23
IGJ main design principles




Transitivity: The design must provide
transitive (deep) immutability
Purely static: There should be no runtime
representation for immutability
Polymorphism: It must be possible to
abstract over immutability without code
duplication
Simplicity: The design should not change
Java's syntax and have a small set of
typing rules
6/23
Type Hierarchies for IGJ
The type hierarchy for
immutability parameters
The top of the type hierarchy
for all other classes
7/23
IGJ Subtype hierarchy
Legend:
L List, O object, R ReadOnly
IM Immutable, M Mutable
For example:
L< R,O<M> > means
List<ReadOnly, Object<Mutable>>
// Demonstrates how to copy value of readonly roObj to mutable mutableObj
Object<ReadOnly> roObj = ...;
List<Mutable,Object<Mutable>> l = new List<Mutable,Object<Mutable>>();
((List<Mutable,Object<ReadOnly>>) l).add(roObj);
Object<Mutable> mutableObj = l.get(0); // mutableObj equals roObj
8/23
Java Array Co-Variance Problem
// A is a single-element array of String.
String[] a = new String[1];
// B is an array of Object
Object[] b = a;
// Assign an Integer to b. This would be possible if b really were
// an array of Object, but since it really is an array of String,
// we will get a java.lang.ArrayStoreException.
b[0] = new Integer (1);
Read from Array: OK!
Write to Array: Problem!
Solution with IGJ –
immutability promise us
only reading  no Co-Variance problem
9/23
The Field Rule
Typing is guaranteed by several rules.
Let I(x) denote the immutability of x
Rule I: Field Assignment Rule
o.someField = exp;
legal iff I(o) = Mutable.
Example:
Employee<ReadOnly> roE = ...;
roE.address = ...; // Compilation error!
10/23
"Immutability" of Methods




4 new annotations: @ReadOnly,
@Mutable, @Immutable and
@AssignFields
Example:
@Mutable void m() {...this...}
Here: I(this) is Mutable
In general: in any method m, I(this) is
the same as I(m)

“this” immutability depends on the context
11/23
Reference-Immutability Rules

Method Invocation Rule:
o.m(...) is legal if I(o) is subtype of I(m).

(not necessarily I(o) = I(m) )
Employee<Mutable> o = ...;
o.setAddress(...); // OK since I(o) = Mutable and I(setAddress) = Mutable
o.getAddress(); // OK since I(o) = Mutable and I(getAddress) = ReadOnly
((Employee<ReadOnly>) o).setAddress(...); // Compilation error!
12/23
Example
IGJ classes Edge<I> and Graph<I>, with the immutability
parameters (and annotations, for this) underlined.
1: class Edge<I extends ReadOnly> {
2:
private long id;
3:
public @AssignFields Edge(long id) { this.setId(id); }
4:
public @AssignFields synchronized void setId(long id) {
5:
this.id = id; }
6:
public @ReadOnly synchronized long getId() { return id; }
7:
public @Immutable long getIdImmutable() { return id; }
8:
public static void print(Edge<ReadOnly> n) {... }
9: }
For now:
10: class Graph<I extends ReadOnly> { Assume @Immutable is like @ReadOnly
11:
public Edge<I> lastN;
And @AssignFields is like @Mutable
12:
public List<I,Edge<I>> l;
13:
public @AssignFields Graph(List<I,Edge<I>> l) { this.l = l; }
14:
public @Mutable void addEdge(Edge<I> n) {
15:
this.l.add(n); this.lastN = n; }
16:
public @ReadOnly Edge<I> getLast() { return this.lastN; }
17:
public static <T extends ReadOnly>
18:
Edge<T> findEdge(Graph<T> nl, long id) { ... }
19: }
13/23
Example:
1: class Edge<I extends ReadOnly> {
2:
private long id;
3:
public @AssignFields Edge(long id) { this.setId(id); }
4:
public @AssignFields synchronized void setId(long id) {
5:
this.id = id; }
6:
public @ReadOnly synchronized long getId() { return id; }
7:
public @Immutable long getIdImmutable() { return id; }
8:
public static void print(Edge<ReadOnly> n) {... }
9: }




Line 5: the assignment into this.id is OK
If this.id = …; was on line 6 – illegal…
Line 3: OK due to Method Rule
Line 8: static  no annotation, Edge of any
immutability could be pass here…
14/23
Example:
10: class Graph<I extends ReadOnly> {
11:
public Edge<I> lastN;
12:
public List<I,Edge<I>> l;
13:
public @AssignFields Graph(List<I,Edge<I>> l) { this.l = l; }
14:
public @Mutable void addEdge(Edge<I> n) {
15:
this.l.add(n); this.lastN = n; }
16:
public @ReadOnly Edge<I> getLast() { return this.lastN; }
17:
public static <T extends ReadOnly>
18:
Edge<T> findEdge(Graph<T> nl, long id) { ... }
19: }



Line 11: a class can pass its immutability parameter to
its fields
Line 16: Also return type – no need for overloading
Line 12: Transitivity - in an immutable Graph the field l
will contain an immutable list of immutable edges
15/23
Object Immutability & constructors

What annotation should CTOR be?...

@Mutable? problem:
public @Mutable Graph(List<I,Edge<I>> l) {
this.l = l;
this.addEdge( new Edge<Mutable>(0) ); // 
}
…
List<Immutable,Edge<Immutable>> imList = ...;
new Graph<Immutable>(imList); // An element was added
to imList

@Immutable? Guess not…
16/23
Object Immutability & constructors


Solution: Forth kind of reference
immutability: AssignFields
Permit to perform limited side-effects
without permitting modification of
immutable objects


@Mutable method can assign & mutate
@AssignFields method can only assign
17/23
Immutability & Assignability

MyClass myObject = new MyClass();

myObject = anotherObject;


Assignability
myObject.setField(4);

immutability
18/23
Revised rules

Field Rule revised (relaxed):

AssignField is not transitive…
o.someField = ...; is legal if I(o) = Mutable
or (I(o) = AssignFields and o=this)

Method Rule revised (restricted):
o.m(...) is legal if I(o) is subtype of I(m)
and (I(m) = AssignFields implies o=this)
19/23
Example:
1: class Edge<I extends ReadOnly> {
2:
private long id;
3:
public @AssignFields Edge(long id) { this.setId(id); }
4:
public @AssignFields synchronized void setId(long id) {
5:
this.id = id; }
6:
public @ReadOnly synchronized long getId() { return id;}
7:
public @Immutable long getIdImmutable() { return id; }
8:
public static void print(Edge<ReadOnly> n) {... }
9: }


Line 5: the assignment into this.id is still OK
setId is annotated with @AssignFields 
I(this)=AssignFields
Line 3: I(this) = AssignFields & I(setId) =
AssignFields
20/23
Example:
public @mutable Graph(List<I,Edge<I>> l) {
this.l = l;
this.l.get(0).setId(42); // 
}


Line 13: If we will add the following code – it will be
illegal in the revised rule (and legal in the old one)
New Rule:
new SomeClass<X,…>(…) is legal only if



X = Mutable and this CTOR is not marked as @Mutable, or
X = Imuutable and this CTOR is not marked as @Immutable
(X = readOnly & X=AssignFileds are illegal)
21/23
Future Work



Plug-in for IDE (e.g. Eclipse)
A WriteOnly immutability parameter
@readable notation for field
class Vector<I extends None, T> {
@readable int size; ...
@None int size() { return size; }
@WriteOnly void add(T t) { ... }
@WriteOnly void removeLast() { ... }
@Mutable void remove(T t) { ... }
@ReadOnly void get(int index) { ... }
}
22/23
Future Work (cont.)

Add default immutability
class Graph<I extends ReadOnly default Mutable>

An alternative syntax (Java 7?...)
@immutable Document[@readonly]
new @mutable ArrayList<@immutable Edge>(...)

Runtime support (e.g. down-cast)
23/23