Home

A Checker Framework tutorial

Welcome!

This is a hands-on, play-along tutorial for null-safe Java programming with the Checker Framework.

Read on for the what and why, or skip to the practical part which begins with the Setup.

Imagine

Imagine you have created a neat little utility that turns the string A wonderful autumn afternoon into a-wonderful-autumn-afternoon:

public static String makeSlug(String s) {
    return s.replaceAll("\\s+", "-").toLowerCase();
}

Somewhere else in the code this utility is used to create a page title:

    String title = hasTitle()
            ? getTitle()
            : System.getProperty("defaults.title");

    String titleSlug = makeSlug(title);

What could go wrong?

If you have been programming Java for any amount of time, that call to makeSlug() should make you a little queasy: this code may blow up with a NullPointerException.

Though it isn’t explicit about it, makeSlug does not accept a null argument. Just from reading the code we know that at the point where makeSlug(title) gets evaluated, title might very well be null. Therefore the code is not correct.

This is the kind of reasoning we do every day: read the code and track which references may be null at a given point to make sure the code is correct.

Wouldn’t it be nice if this sort of reasoning about what may and may not be null could somehow be expressed in code? And wouldn’t it be nice to have a machine check the flow of ‘possibly null’ and ‘definitely not null’ references for us, and establish whether the code is correct with respect to null?

This is where the Checker Framework comes in.

The Checker Framework

The Checker Framework is a static analysis tool for people who care about safe, correct code.

The Checker Framework consists of a number of ‘checkers’ (technically, annotation processors) that hook into the compilation process. Each checker makes a promise to check something at compile time that would normally only be detected at run-time. There are checkers for nullness, regex syntax, format strings, synchronisation locks, and so on.

To make this checking work, we need to make some of our knowledge about the code explicit through annotations. As an example, the Regex Checker checks the syntax and usage of strings representing regular expressions.

@Regex String digitPattern = "\\d+";

Provided that @Regex strings are all annotated properly, you get a compile-time guarantee that no errors from mistaken regex syntax will arise at run-time.

The checker we are going to use is the Nullness Checker, and its promise is to eliminate all nullness errors like the NullPointerException we saw at the beginning.

This tutorial

This is an interactive tutorial for you to follow along on your machine.

• We will set up a little real-world project and incorporate the Checker Framework into the build. The checker will report errors, and we will interpret the diagnostics, discuss, and fix some bugs.
• The entire play-along part is encapsulated nicely in the Git log for reference.
• I promise to give a summary of achievements (annotations added, bugs fixed) at the end.

On to the mission statement on the next page.

---

This work is licensed under a Creative Commons Attribution 4.0 International License.