I returned to Hilton Yosemite A/B/C to see two speakers from the University of Washington [1] Computer Science and Engineering [2] (Werner Dietl [3] and Michael Ernst [4]) speak on The Checker Framework [5] in a presentation called "Build Your Own Type System for Fun and Profit."
Ernst started off the presentation and showed images demonstrating that we can seen undesired errors and stack traces on the web, on the desktop, and even on mobile devices. With this background in mind, he introduced the idea of a "pluggable type system" to address Java "being too weakly typed."
The Checker Framework [7] "plugs a type checker into the Java compiler" and is used with the standard javac [8] command-line compiler tool. New annotations can be used today (before Java 8/JSR 308 [9] general availability) because they can be commented out with /* */ comment syntax and the Checker Framework will respect them. Then, when Java 8 is released with this new type support [10], these can be uncommented and the language compiler will allow annotations to be specified against types. This means that Checker Framework's annotations can be used directly (not commented out) on types in JDK 8 (but Checker Framework will not itself be part of JDK 8).
It is important to emphasize the value of this: using Checker Framework [11] and provided compiler plug-ins allows errors and exceptions that would normally not be seen until runtime (and then perhaps sporadically) to be seen consistently and earlier at compile time. The presentation was organized to present the runtime (mis)behaviors that we desire to avoid followed by what operations are legal for each misbehavior and the types of data that lead to that problem.
The speakers ran their Checker Framework against millions of lines of source code and used a consistent approach. This approach included the differentiation of real problems found versus problems with the annotation.
@NonNull and @Nullable are part of the "Null Pointer Exception type system." They found that Google Collections [12]'s ForMapWithDefault class has an @Nullable field called defaultValue that is (by implicit default) initialized to null, but then is dereferenced in the hashCode() implementation. The FindBugs [13] runs against this code and the many unit tests written against this code had not detected this issue. Use of annotations such as these is another good tactic for effective NullPointerException handling [14].
Ernst talked about avoiding ClassNotFoundException and outlined four types of data (unqualified strings, fully qualified names, binary names, and field descriptors). The Javadoc for java.lang.class.forName() states that the provided String is the "fully qualified name of the desired class." However, it really should have been documented as binary name. The only way this problem is encountered in runtime is when an anonymous class is used, but it will have an error in that case. Related to this particular issue, they found 24 errors in OpenJDK and other libraries.
Dietl started by talking about the "regular exprsesion type system." The effort here is to avoid PatternSyntaxException and IndexOutOfBoundsException. This can be done using two annotations: @Regex and @Unqualified.
After showing Checker Framework code and its use by demonstration, Dietl asked the audience for other useful runtime errors they'd like to have. Ernst "got so excited" in responding that he temporarily left the methodology, but the point was still made: Checker Framework already supports detection of numerous common runtime issues at compile time, but is extensible for new or yet undiscovered runtime issues.
Dietl talked about a sample of type checkers including @Tainted, @BinaryName, @Nullable, @Lock, @GuardBy, @Immutable, @SwingCompassDirection (fake enumerations), @Localized (internationalization), @RegEx, etc.
Dietl moved onto showing how to develop one's own type system and used creation of an "Encryption type system" to demonstrate this. He showed four lines of code that completely implement the checker to make sure that only encrypted Strings are sent.
Ernst explained that more complicated checkers can be created. Complex checkers can consist of multiple checkers. The Checker Framework has built-in "powerful analyses" that can be used by all checkers.
Ernst talked about other tools built into Checker Framework and then summarized pluggable type checking as one approach to building quality code. The Checker Framework is a pluggable type checker that can be extended for personal and custom needs. There are three simple questions (What runtime behavior?, What operations are legal?, What is the data?) whose answers can make working with types easier.
One interesting question and response led to Ernst's statement that the Checker Framework is best suited for quality issues related to data, but not to structure.
Another question brought up two actual questions. One question was about why Checker Framework reports warnings rather than errors, but Ernst stated that there is a switch to change it to report them as errors. The second question was about integration of Checker Framework with Eclipse. Eclipse has its own compiler, but there is a "mostly functionality" Eclipse plugin that can be used to support Eclipse use of Checker Framework.
Any version of Java can be compiled with Checker Framework and Java 8 will even support special syntax for this. The reasons that this is not a standard part of the language include that not everyone wants it and not everyone can agree on the definitions. "Because different people need different things," it is not desirable to standardize all of the checkers. JSR 305 [15] ("Annotations for Software Defect Detection") is Dormant [16] currently.
There are many things I've excited to use sometime in the future such as the JDK 8 features of Project Lambda [17] and JSR 310 Date/Time API [18], but I am really excited to try using Checker Framework immediately to improve my code's quality! I like it when my experiences at JavaOne do include exciting things for the intermediate to long term future as well as some try-it-right now experiences.
Original posting available at http://marxsoftware.blogspot.com/ [19] (Inspired by Actual Events)
Links:
[1] http://www.washington.edu/
[2] http://www.cs.washington.edu/
[3] http://homes.cs.washington.edu/~wmdietl/
[4] http://homes.cs.washington.edu/~mernst/
[5] http://types.cs.washington.edu/checker-framework/
[6] http://3.bp.blogspot.com/-_eGYTisXQ5I/UGs-HX-gsiI/AAAAAAAADgk/1TTO4g5OjiA/s1600/IMG_20121002_075641-taylorStreet-smallerResolution.jpg
[7] http://types.cs.washington.edu/checker-framework/current/checkers-manual.html
[8] http://docs.oracle.com/javase/7/docs/technotes/guides/javac/index.html
[9] http://jcp.org/en/jsr/detail?id=308
[10] http://types.cs.washington.edu/jsr308/
[11] http://types.cs.washington.edu/checker-framework/current/checkers-manual.pdf
[12] http://code.google.com/p/google-collections/
[13] http://findbugs.sourceforge.net/
[14] http://marxsoftware.blogspot.com/2009/04/effective-java-nullpointerexception.html
[15] http://jcp.org/en/jsr/detail?id=305
[16] http://jcp.org/en/jsr/stage?listBy=dormant
[17] http://marxsoftware.blogspot.com/2012/10/javaone-2012-road-to-lambda.html
[18] http://marxsoftware.blogspot.com/2012/10/javaone-2012-from-instants-to-eras.html
[19] http://marxsoftware.blogspot.com/
