The Checker Framework tool supports the processing of custom-built annotations for Java at compile time. This paper reports on a case study using the tool to build five checkers. The ease of building, the ease of use, and the effectiveness of each checker are discussed at length. An informal report is provided on classroom use of the Nullness checker.

Figure 1 presents the case study statistics. Four of the five checkers were small in size, but the Nullness checker comprised over 4,000 lines of code. The number of annotations written for each program in the case study was typically over 100. Defects capable of causing runtime failure were found in more than half of the programs. Other kinds of errors, such as incorrect documentation, were found in most programs. The false positive rate was over 50 percent for eight of the 11 programs studied. In the classroom study, all students found at least one null pointer defect. The majority of students, however, only used the two annotations they had been taught (@NonNull and @Nullable).

The authors conclude that the five checkers were easy to build and use. Since time was not used as a measure, particularly the time needed to identify and suppress false positives, these claims could be disputed. However, readers will be impressed by the detection of over 40 defects in well-tested and well-used programs. These checkers found defects for Google Collections that had been missed by the FindBugs static analysis tool. This paper is strongly recommended to the software engineering community.