OOPSLA '04

Program
Technical Program
  Invited Speakers
  Technical Papers
  Onward!
  Panels
  Practitioner Reports
  Tutorials
Workshops
DesignFest
Educators' Symposium
Demonstrations
Posters
Doctoral Symposium
Exhibits
Student Research Comp.
FlashBoF
 
Turing Lecture
 
Social Events
 
Week at a Glance
 
Final Program (1.5M .pdf)

Find in Program
 

Page
Printer-friendly

Basket
view, help

"A Practical Type System and Language for Reference Immutability"
Object-Oriented Programming, Systems, Languages and Applications
Home    Program    Housing & Transportation    Registration    Submissions    Wiki    Maps
 
  > Technical Program > Technical Papers > Generics

 : Tuesday

A Practical Type System and Language for Reference Immutability

Ballroom A-B
Tuesday, 11:30, 30 minutes
 


 
7·8·9·10·11·12·13·14·15·16·17·18·19·20·21

Adrian Birka, MIT
Michael D. Ernst, MIT

This paper describes a type system that is capable of expressing and enforcing immutability constraints. The specific constraint expressed is that the abstract state of the object to which an immutable reference refers cannot be modified using that reference. The abstract state is (part of) the transitively reachable state: that is, the state of the object and all state reachable from it by following references. The type system permits explicitly excluding fields or objects from the abstract state of an object. For a statically type-safe language, the type system guarantees reference immutability. If the language is extended with downcasts, then run-time checks enforce the reference immutability constraints.

In order to better understand the usability and efficacy of the type system, we have implemented an extension to Java, called Javari, that includes all the features of our type system. Javari is interoperable with Java and existing JVMs. This paper describes the design and implementation of Javari, including the type-checking rules for the language. This paper also discusses experience with 160,000 lines of Javari code; Javari was easy to use and provided a number of benefits, including detecting errors in well-tested code.