@Nullable and @NotNull in JHotDraw

This spring I participated in the course formal methods and functional programming at ETH Zurich.

A major subject of this course were correctness proofs of algorithms.With proofs we can show the correctness of a program. This is in contrast to testing, which can only show the presence of errors, but not their absence.

The ultimate goal is showing the complete correctness of a software application. This is not possible as of today, but major progress has been done in this area for .NET with the Spec# programming system. Among many more advanced things, with Spec# we can show the absence of null pointer errors in a program.

For Java, the IDEA IDE supports @Nullable and @NotNull annotations. A proofer is built into the editor and highlights potential null pointer errors directly in the code.

Since I didn’t want to include IDEA code with another license model into JHotDraw, and since I wanted to tinker a little bit with the concept, I have created a new annotations package in JHotDraw 7.5.1.

My @Nullable and @NotNull annotations are almost identical to the ones in IDEA. The only difference is, that the annotations can be set on classes as well. Usually, I set a @NotNull annotation on a class, to say that – by default – all types and methods defined by this class are non-null. And then, I set the @Nullable annotation to define exceptions of this rule. This nicely keeps down the number of annotations needed in a Java class.

I haven’t yet used these annotations on many classes in JHotDraw, but I plan to use them everywhere in this project.

Update 2011-01-07: In the meantime I dropped my annotation package and  use now FindBugs annotations in many places in JHotDraw 7. FindBugs annotations can be defined at various levels in the source code – for example on a method, a class or on a complete package. This keeps the source code tidy. The FindBugs analyzer can use these annotations to find potential problems in the code. I have fixed all problems that I considered potentially ‘harmful’.