| Program |
 |
|
|
|
| Find in Program |
|
|
|
|
| Page |
|
|
|
|
| Basket |
|
|
view, help
"A Practical Type System and Language for Reference Immutability"
|
|
|
|
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.
|
