These are some common questions about the Type Annotations (JSR 308) extension to Java. Feel free to suggest improvements to the answers, or other questions to include here.
Before you read this FAQ, you should probably read either the Type Annotations Specification (if you are most interested in the language syntax) or the Checker Framework Manual (if you are most interested in pluggable type-checking). Then, if you still have questions, you can see whether this FAQ answers them.
Contents:
Type annotations make Java's annotation system more expressive and uniform. Thus, they can be used for many of the same purposes as Java 5 annotations. A new use is as type qualifiers. Programmers can write these type qualifiers in their programs, and then a compiler plug-in automatically finds bugs.
No tool will solve all your problems, but pluggable type-checkers have been shown to help programmers to rid their programs of certain important classes of bugs, including null pointer errors, incorrect side effects, incorrect equality tests, and more. Users of the Checker Framework keep noticing new ways that pluggable type-checkers are useful, and you probably will too.
For more details, see the Checker Framework Manual and also section Example use of type annotations: Type qualifiers in the Type Annotations Specification.
The paper Practical pluggable types for Java discusses case studies in which programmers found type annotations to be natural to read and write. The code continued to feel like Java, and the type-checking errors were easy to comprehend and often led to real bugs.
You don't have to take our word for it, though. You can try the Checker Framework for yourself.
The difficulty of adding and verifying annotations depends on your program. If your program is well-designed and -documented, then skimming the existing documentation and writing type annotations is extremely easy. Otherwise, you may find yourself spending a lot of time trying to understand, reverse-engineer, or fix bugs in your program, and then just a moment writing a type annotation that describes what you discovered. This process inevitably improves your code. You must decide whether it is a good use of your time. For code that is not causing trouble now and is unlikely to do so in the future (the code is bug-free, and you do not anticipate changing it or using it in new contexts), then the effort of writing type annotations for it may not be justified.
As with any language feature, it is possible to write ugly code that over-uses annotations. However, in normal use, very few annotations need to be written. Figure 1 of the paper Practical pluggable types for Java reports data for over 350,000 lines of type-annotated code:
Furthermore, these numbers are for annotating existing code. New code that is written with the type annotation system in mind is cleaner and more correct, so it requires even fewer annotations.
In other words, annotations do not clutter code, and they are used much less frequently than generic types, which Java programmers find acceptable.
Pluggable type-checking is a motivating application for type annotations. But a pluggable type-checker is a separate tool that is not specified as part of Java itself.
Each checker looks for certain errors. You can use multiple checkers, but even then your program might still contain other kinds of errors.
If you run a pluggable checker on only part of the code of a program, then you do not get a guarantee that all parts of the program satisfy the type system (that is, are error-free). An example is a framework that clients are intended to extend. In this case, you should recommend that clients run the pluggable checker. There is no way to force users to do so, so you may want to retain dynamic checks or use other mechanisms to detect errors.
There are other circumstances in which a static type-checker may fail to detect a possible type error. In Java, these include arrays, casts, raw types, reflection, separate compilation (bytecodes from unverified sources), native code, etc. (For details, see section What the checker guarantees in the Checker Framework manual.) Java uses dynamic checks for most of these, so that the type error cannot cause a security vulnerability or a crash. The pluggable type-checkers inherit many (not all) of these weaknesses of Java type-checking, but do not currently have built-in dynamic checkers. Writing dynamic checkers would be an interesting and valuable project.
Even if a tool such as a pluggable checker cannot give an ironclad guarantee of correctness, it is still useful. It can finding errors, excluding certain types of possible problems (e.g., restricting the possible class of problems), and increasing confidence in a piece of software.
In brief, use subtypes when you can, and type qualifiers when you cannot. For more details, see section When to use (and not use) type qualifiers in the Checker Framework manual.
You can use the checkers that are distributed with the Checker Framework, or you can write your own to check specific properties that you care about. Thus, you can find and prevent the bugs that are most important to you.
Section How to create a new checker in the Checker Framework Manual gives complete details regarding how to write a checker. It also suggests places to look for more help, such as the Checker Framework API documentation (Javadoc) and the source code of the distributed checkers.
To whet your interest and demonstrate how easy it is to get started, here is an example of a complete, useful type checker.
@TypeQualifier @SubtypeOf(Unqualified.class) public @interface Encrypted { }
Section Basic checker example in the Checker Framework Manual explains this checker and tells you how to run it.
Pluggable type-checking finds more bugs than a bug detector does, for any given variety of bug.
A bug detector like FindBugs, JLint, or PMD aims to find some of the most obvious bugs in your program. It uses a lightweight analysis, then uses heuristics to discard some of its warnings. Thus, even if the tool prints no warnings, your code might still have errors — maybe the analysis was too weak to find them, or the tool's heuristics classified the warnings as likely false positives and discarded them.
A type checker aims to find all the bugs (of certain varieties). It requires you to write type qualifiers in your program, or to use a tool that infers types. Thus, it requires more work from the programmer, and in return it gives stronger guarantees.
Each tool is useful in different circumstances, depending on how important the desired level of confidence in your code. For more details on the comparison, see section Comparison to other tools in the Checker Framework manual. For a case study that compared the nullness analysis of FindBugs, JLint, PMD, and the Checker Framework, see section 6 of the paper “Practical pluggable types for Java”.
JML, the Java Modeling Language, is a language for writing formal specifications. JML aims to be more expressive than pluggable type-checking. JML is not as practical as pluggable type-checking.
A programmer can write a JML specification that describes arbitrary facts about program behavior. Then, the programmer can use formal reasoning or a theorem-proving tool to verify that the code meets the specification. Run-time checking is also possible. By contrast, pluggable type-checking can express a more limited set of properties about your program.
The JML toolset is less mature. For instance, if your code uses generics or other features of Java 5, then you cannot use JML. However, JML has a run-time checker, which the Checker Framework currently lacks.
Type annotations will be a part of the Java 7 language.
As of build b64 (publicly released on July 9, 2009), Sun's OpenJDK supports type annotations. The Type Annotations Compiler is a variant of the OpenJDK compiler with same extra features for compatibility with non-Java-7 compilers. It is distributed standalone or as part of the Checker Framework.
You can use type annotations and custom type-checkers even if your coworkers and users do not use custom type-checkers or the Type Annotations compiler. You simply write the annotations in comments and use the Type Annotations compiler, which recognizes comments containing type annotations. Other developers can compile the annotated code using any Java compiler, which will ignore the type annotations. The Type Annotations compiler produces bytecodes that are identical to those produced by javac, so the .class files can be used in any JVM. This also gives you an easy way to convince your colleagues to try type annotations and the Checker Framework. For more details, see section Writing annotations in comments for backward compatibility in the Checker Framework Manual.
We have had successful reports from users of all three platforms. If you have trouble installing or running the tools, please report a bug. The Community section of the Type Annotations webpage explains how.
Full Type Annotation support is not yet available for the Eclipse compiler. However, prototype support is available. See the Eclipse section of the Checker Framework Manual for details.
Preliminary support (green parsing of type annotations) is planned for the summer 2009 EAP (Early Access Programs) builds of the IDEA 9.
See the Community section of the Type Annotations webpage.
An annotation before a method sometimes refers to the return type, and sometimes to the method itself. There is never any ambiguity regarding which is intended. See section Disambiguating type and declaration annotations in the Type Annotations specification.
If you are skeptical of the usefulness of the annotations, see section Uses for annotations on types in the Type Annotations specification.
If you are skeptical of the syntax of array annotations, then perhaps you really don't like Java's array syntax. The annotation extension is a logical extension of Java's syntax; see section Syntax of array annotations in the Type Annotations specification.
If you are skeptical of the syntax of receiver annotations, then see section Receivers in the Type Annotations specification.
While these annotations are critical in important circumstances, they are not extremely common in well-written code. And you don't have to use them if you don't want to.
Objects are not annotated — types or declarations are. Java has no run-time representation of the types of the variables that refer to an object. The Type Annotations specification (JSR 308) enriches types, but it does not change that fundamental property. Type annotations as implemented in JSR 308 have no run-time representation. This means that they impose no run-time burden on Java programs that use them.
Reflective calls can query the class of an object, or can query the type annotations on source code.
Type Annotations (JSR 308) is a language extension that makes existing and future annotations more useful to programmers. By contrast, Annotations for Software Defect Detection (JSR 305) defines some specific annotations, such as @Nonnull and @Positive. The JSR 305 annotations are most useful if they can be written on types, so JSR 305 needs JSR 308 to achieve its full potential. For a more detailed comparison, see section Semantics of annotations in the Type Annotations specification.
The Type Annotations (JSR 308) language extension permits you to write annotations in new locations. This syntax makes possible new sorts of tools, such as pluggable type-checking. The Checker Framework enables you to create and use pluggable type-checkers.
Implementing pluggable type-checking would be impractical without the Type Annotations syntax, but the Checker Framework is an independent tool and not a part of the Type Annotations proposal. The Checker Framework distribution includes the Type Annotations compiler for convenience, so that users only have to download and install one file.
Statement annotations are within the scope of JSR 308, and this feature is under consideration. See the section Annotations on Statements in the Type Annotations specification.
Perhaps it should. See section Other possible extensions to Java annotations in the Type Annotations Specification. Feel free to suggest modifications or additions to that section. Your edits should correct factual errors, or should be well-motivated by compelling use-cases that cannot be achieved by other means.
The Type Annotations (JSR 308) expert group gladly welcomes suggestions for improvements to the Type Annotations specification, and to the tools that support it. See section Other possible extensions to Java annotations in the Type Annotations Specification.
Defining annotations is beyond the scope of the Type Annotations Specification, whose purpose is to lay the groundwork so that others can define such types.
A JSR, or Java Specification Request, is a proposed specification for some aspect of the Java platform — the Java language, virtual machine, libraries, etc. For more details, see the Java Community Process FAQ. Many people refer to the Type Annotations specification by its Sun codename, “JSR 308”.
Last updated: June 28, 2009.
Back to the Type annotations (JSR 308) webpage.