-
Notifications
You must be signed in to change notification settings - Fork 6
Home
Welcome!
This is a hands-on, play-along tutorial for null-safe programming with the Checker Framework.
Suppose 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 app 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, the call to
makeSlug()
probably has you shifting around uneasily: this code may blow up
with a NullPointerException
.
Though it doesn't make it explicit, makeSlug
does not accept a null
argument. Just from reading the code we can see 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 at a given place in the code could somehow be expressed in code? And wouldn't it be nice to have a machine check the flow of possibly null and definitely non-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 consists of a number of ‘checkers’ 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, for regexps, for format strings, and so on. For this to work, some things need to be made explicit through annotations.
The Regex Checker, for example, checks the syntax and usage of Strings representing a regular expression.
@Regex String digits = "\\d+";
Provided that you have annotated your @Regex
es properly, you get a compile
time guarantee that no errors from mistaken use of regexps arise at runtime.
The checker we're going to use is the Nullness Checker, and it promises to
eliminate any errors like the NullPointerException
we saw at the beginning.
todo
Mission statement on the next page.