Prof. Dr. Michael Ernst

"Preventing bugs with pluggable type-checking"

Type-checking helps to detect and prevent errors. However, a programming language's built-in types are often incapable of expressing important information, such as whether a variable may be null, whether a value is intended to be side-effected, or whether a String is interned. As a result, a type-correct program can suffer from null pointer exceptions, incorrect mutations, errors in equality testing, and many other types of problems.
User-definable extensions to the type system -- pluggable types -- can detect such errors, prevent them, or verify their absence. We present the first practical pluggable type system that integrates with a practical object-oriented programming language. Our framework works for Java, but the ideas are applicable to other languages. While the framework is compatible with all versions of the language, Java 7 will contain syntactic support for it, in the form of type annotations. Our system provides benefits to two communities.
* For programmers, it improves documentation and eliminates bugs. Case studies on multiple programs of more than 200,000 lines demonstrate these benefits.
* For type system designers, it makes it easy to implement and deploy a type system in the context of an industrial language. This enables realistic evaluation of research proposals. We illustrate this by presenting new insights about several type systems -- insights that had not been obtained through theoretical consideration or small-scale case studies.