J\mask: Masked types for sound object initialization in Java

Masked types are a type-based solution to the long-standing problem of object initialization. Constructors, the conventional mechanism for object initialization, have semantics that are surprising to programmers and that lead to bugs. They also contribute to the problem of null-pointer exceptions, which make software less reliable. Masked types are a new typestate mechanism that explicitly tracks the initialization state of objects and prevents reading from uninitialized fields. They even work in the presence of cyclic data structures and inheritance. Masked types are a lightweight typestate mechanism that does not require any aliasing information.

Downloads

The J\mask compiler is available for use for research and experimentation.

Papers and reports

Contributors

Support

The development of J\mask has been supported by a number of funding sources, including NSF Grants CNS-0430161 and NSF-0627649 and by Air Force Rome Laboratories under award #FA8750-08-2-0079.

How J\mask works

J\mask is an extension to Java that adds masked types. The type T\f is the type T, but with the field f inaccessible because it might not have been initialized yet. A constructor is just a method with effect * -> T.sub, representing that it changes the mask of this from * (meaning that all fields are uninitialized) to T.sub (meaning that all subclass fields are uninitialized).

In the resulting language, constructors are ordinary methods that operate on uninitialized objects, and no special default value ("null") is needed in the language. Initialization of cyclic data structures is achieved with the use of conditionally masked types that encode a graph reachability problem. Masked types are also modular and compatible with data abstraction, through the use of abstract masks.

Example

Initializing a circularly linked list of size 2: 

class Node {
  Node next;
  Node() effect *! -> *! { }
}

Node\next! x = new Node();
Node\next! y = new Node();
  // can't read x.next or y.next here
x.next = y;
  // x : Node\next[y.next]
  // y : Node\next!
y.next = x;
  // x : Node\next[y.next]
  // y : Node\next[x.next]
  // ==> 
  // x : Node
  // y : Node
  // can read both x.next and y.next here