Tutorial: Preventing Runtime Errors at Compile Time

Werner Dietl and Michael D. Ernst, University of Washington.

This is the companion site to our OSCON session.

Abstract

A pluggable type system extends a language's built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker (in as little as 4 lines of code!); scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques.

While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enables non-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.

Tutorial format

We will:

guide the audience through installing the Checker Framework, including how to set up Eclipse integration;
teach how to use some of the checkers included with the Checker Framework;
discuss other types of errors that one would like to be prevented at compile time;
and teach how to write a new type checker to prevent the errors we come up with in our discussion.

Audience participation is desired! We expect the audience to come prepared with a laptop with a working Java environment (Eclipse optional).

During our tutorial, we will use the Checker Framework. For the command-line setup, see the installation instructions and tutorial in the Checker Framework manual.
After following those, set the CHECKERS environment variable to the checker-framework/checkers/ directory within your Checker Framework installation.

Resources

Regular Expression Checker demonstration

Demo application: Search.java.

After installing the Checker Framework, type check this application by running:

$CHECKERS/binary/javac -processor checkers.regex.RegexChecker Search.java

Encryption Checker demonstration

You will write your own declarative type checker to ensure encrypted communication!

Demo application: EncryptionDemo.java.

In the session we will write a new Encrypted annotation. You compile it like any other Java class:

$CHECKERS/binary/javac .../Encrypted.java

You then use the Basic Checker to check the demo program, like so:

$CHECKERS/binary/javac -processor checkers.basic.BasicChecker -Aquals=encrypted.quals.Encrypted .../EncryptionDemo.java

[It is sometimes necessary to provide the location of the annotation class on the bootclasspath. Use the "-Xbootclasspath/p:yourpath" parameter for this.]

Personal Blog demonstration

As a first demonstration, we will use the Personal Blog demonstration. You can download the project here. Unzip it into a directory. An Ant build file is there. In Eclipse, you can import the folder as a new project.

Feel free to contact us! Email checker-framework-dev@googlegroups.com

Last updated: July 17, 2012