Annotations on Java types

JSR 308 working document
Michael D. Ernst
mernst@csail.mit.edu
August 1, 2007

This document is available in PDF format at https://checkerframework.org/jsr308/java-annotation-design.pdf.

The JSR 308 webpage is https://checkerframework.org/jsr308/. It contains the latest version of this document, along with other information such as links to the prototype implementation.

Contents:


1  Introduction

We propose an extension to Java's annotation system [Bra04a] that permits annotations to appear on any use of a type. (By contrast, Java SE 6 permits annotations to appear only on class/method/field/variable declarations; our proposal is backward-compatible and continues to permit those annotations.) Such a generalization removes arbitrary limitations of Java's annotation system, and it enables new uses of annotations. The proposal also notes a few other possible extensions to annotations (see Section 7).

This document specifies the syntax of extended Java annotations, but it makes no commitment as to their semantics. As with Java's existing annotations [Bra04a], the semantics is dependent on annotation processors (compiler plug-ins), and not every annotation is necessarily sensible in every location where it is syntactically permitted to appear. This proposal is compatible with existing annotations, such as those specified in JSR 250, ``Common Annotations for the Java Platform'' [Mor06], and JSR 305, ``Annotations for Software Defect Detection'' [Pug06]. (For a comparison of JSR 305 and JSR 308, see Section 9.3.)

This proposal does not change the compile-time, load-time, or run-time semantics of Java. It does not change the abilities of Java annotation processors as defined in JSR 269 [Dar06]. The proposal merely makes annotations more general --- and thus more useful for their current purposes, and also usable for new purposes that are compatible with the original vision for annotations [Bra04a].

JSR 308 ``Annotations on Java Types'' [EC06] has the goal of refining the ideas presented here. This proposal serves as a starting point for the JSR 308 expert group, but the expert group has the freedom to modify this proposal or to explore other approaches. (A JSR (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 at https://jcp.org/en/introduction/faq.)

This document first motivates annotations on types by presenting one possible use, type qualifiers (Section 2). Then, it proposes minor changes to the Java language annotation syntax (Section 3) and class file format (Section 4). Section 5 describes the modifications to the JDK necessitated by the Java and class file changes, and Section 6 discusses how these changes will be tested. The document concludes with discussion of other annotations that may be included in future revisions of JSR 308 (Section 7), logistical matters relating to incorporation in the Sun JDK (Section 8), issues that are out of scope for JSR 308 (Section 9), and related work (Section 10).

2  Example use of type annotations: Type qualifiers

One example use of annotation on types is to create custom type qualifiers for Java, such as @NonNull, @ReadOnly, @Interned, or @Tainted. Type qualifiers are modifiers that provide extra information about a type or variable. A designer can define new type qualifiers using Java annotations, and can provide compiler plug-ins to check their semantics (for instance, by issuing lint-like warnings during compilation). A programmer can then use these type qualifiers throughout a program to obtain additional guarantees at compile time about the program. The type system defined by the type qualifiers does not change Java semantics, nor is it used by the Java compiler or run-time system. Rather, it is used by the checking tool, which can be viewed as performing type-checking on this richer type system. (The qualified type is usually treated as a subtype or a supertype of the unqualified type.) Type qualifiers can help prevent errors and make possible a variety of program analyses. Since they are user-defined, developers can create and use the type qualifiers that are most appropriate for their software.

A system for custom type qualifiers requires extensions to Java's annotation system, described in this document; the existing Java SE 6 annotations are inadequate. Similarly to type qualifiers, other pluggable type systems [Bra04b] and similar lint-like checkers also require these extensions to Java's annotation system.

Our key goal is to create a type qualifier system that is compatible with the Java language, VM, and toolchain. Previous proposals for Java type qualifiers are incompatible with the existing Java language and tools, are too inexpressive, or both. The use of annotations for custom type qualifiers has a number of benefits over new Java keywords or special comments. First, Java already implements annotations, and Java SE 6 features a framework for compile-time annotation processing. This allows our system to build upon existing stable mechanisms and integrate with the Java toolchain, and it promotes the maintainability and simplicity of our modifications. Second, since annotations do not affect the runtime semantics of a program, applications written with custom type qualifiers are backward-compatible with the vanilla JDK. No modifications to the virtual machine are necessary.

2.1  Examples of type qualifiers

The ability to place annotations on arbitrary occurrences of a type improves the expressiveness of annotations, which has many benefits for Java programmers. Here we mention just one use that is enabled by extended annotations, namely the creation of type qualifiers. (Figure 1 gives an example of the use of type qualifiers.)


 1  @NonNullDefault  
 2  class DAG {
 3
 4      Set<Edge> edges;		
 5
 6      // ...
 7
 8      List<Vertex> getNeighbors(@Interned @Readonly Vertex v) @Readonly { 
 9          List<Vertex> neighbors = new LinkedList<Vertex>();
10          for (Edge e : edges)		
11              if (e.from() == v)                          
12                  neighbors.add(e.to());      
13          return neighbors;			
14      }
15  }

Figure 1: The DAG class, which represents a directed acyclic graph, illustrates how type qualifiers might be written by a programmer and checked by a type-checking plug-in in order to detect or prevent errors.
(1) The @NonNullDefault annotation (line 1) indicates that no reference in the DAG class may be null (unless otherwise annotated). It is equivalent to writing line 4 as ``@NonNull Set<@NonNull Edge> edges;'', for example. This guarantees that the uses of edges on line 10, and e on lines 11 and 12, cannot cause a null pointer exception. Similarly, the (implicit) @NonNull return type of getNeighbors() (line 8) enables its clients to depend on the fact that it will always return a List, even if v has no neighbors.
(2) The two @Readonly annotations on method getNeighbors (line 8) guarantee to clients that the method does not modify (respectively) its argument (a Vertex) or its receiver (a DAG). The lack of a @Readonly annotation on the return value indicates that clients are free to modify the returned List.
(3) The @Interned annotation on line 8 (along with an @Interned annotation on the return type in the declaration of Edge.from(), not shown) indicates that the use of object equality (==) on line 11 is a valid optimization. In the absence of such annotations, use of the equals method is preferred to ==.


As an example of how our system might be used, consider a @NonNull type qualifier that signifies that a variable should never be assigned null [Det96, Eva96, DLNS98, FL03, CMM05]. A programmer can annotate any use of a type with the @NonNull annotation. A compiler plug-in would check that a @NonNull variable is never assigned a possibly-null value, thus enforcing the @NonNull type system.

@Readonly is another example of a useful type qualifier [BE04, TE05, GF05, KT01, SW01, PBKM00]. Similar to C's const, an object's internal state may not be modified through references that are declared @Readonly. A type qualifier designer would create a compiler plug-in (an annotation processor) to check the semantics of @Readonly. For instance, a method may only be called on a @Readonly object if the method was declared with a @Readonly receiver. @Readonly's immutability guarantee can help developers avoid accidental modifications, which are often manifested as run-time errors. An immutability annotation can also improve performance. For example, a programmer can indicate that a particular method (or all methods) on an Enterprise JavaBean is readonly, using the Access Intents mechanism of WebSphere Application Server.

Additional examples of useful type qualifiers abound. We mention just a few others. C uses the const, volatile, and restrict type qualifiers. Type qualifiers YY for two-digit year strings and YYYY for four-digit year strings helped to detect, then verify the absence of, Y2K errors [EFA99]. Range constraints, also known as ranged types, can indicate that a particular int has a value between 0 and 10; these are often desirable in realtime code and in other applications, and are supported in languages such as Ada and Pascal. Type qualifiers can indicate data that originated from an untrustworthy source [PØ95, VS97]; examples for C include user vs. kernel indicating user-space and kernel-space pointers in order to prevent attacks on operating systems [JW04], and tainted for strings that originated in user input and that should not be used as a format string [STFW01]. A localizable qualifier can indicate where translation of user-visible messages should be performed; similarly, annotations can indicate other properties of its contents, such as the format or encoding of a string. An interned qualifier can indicate which objects have been converted to canonical form and thus may be compared via object equality. Type qualifiers such as unique and unaliased can express properties about pointers and aliases [Eva96, CMM05]; other qualifiers can detect and prevent deadlock in concurrent programs [FTA02, AFKT03]. Flow-sensitive type qualifiers [FTA02] can express typestate properties such as whether a file is in the open, read, write, readwrite, or closed state, and can guarantee that a file is opened for reading before it is read, etc. The Vault language's type guards and capability states are similar [DF01].

3  Java language syntax extensions

In Java SE 6, annotations can be written only on method parameters and the declarations of packages, classes, methods, fields, and local variables. Additional annotations are necessary in order to fully specify Java classes and methods.

3.1  Source locations for annotations on types

Our system extends Java to allow annotations on any use of a type. Our system uses a simple prefix syntax for type annotations: the annotation appears before the type, as in @NonNull String. There are two exceptions to this general rule: a method receiver (this) annotation appears after the parameter list, and annotations on other than the top level of a multi-dimensional array do not all appear before the array type (see Section 3.5).

3.2  Examples of annotation syntax

The following list gives examples of how annotations are written in the source, according to the simple prefix rule explained in Section 3.1. For explanations of what the annotations mean and how they can be used, see Section 3.3.

Absence of an example in this section does not mean that the particular syntax is not supported (but nonetheless it would be nice for the list in this section to be exhaustive). The specific annotation names used in this section, such as @NonNull, are examples only; this document does not define any annotations, merely specifying where they can appear in Java code.

3.3  Uses of annotations on types

We now expand on how some of the annotations on types may be used. Each of these uses is either impossible or extremely inconvenient in the absence of the new locations for annotations proposed in this document. For brevity, we do not give examples of uses for every type annotation. It is worthwhile to permit annotations on all uses of types (even those for which no immediate use is apparent) for consistency, expressiveness, and support of unforeseen future uses. Not every type system (or other system using annotations) may utilize every possible annotation location. For example, a system that fully specifies type qualifiers in signatures but infers them for implementations [GF05] may not need annotations on typecasts, object creation, local variables, or certain other locations. Other systems may forbid top-level (non-type-argument, non-array) annotations on object creation (new) expressions, such as new @Interned Object(). However, the annotation system proposed here is expressive enough to handle arbitrary type qualifiers.

3.4  Disambiguating type and declaration annotations

In the proposed syntax, an annotation before a method declaration annotates either the return type, or the method declaration; similarly for field declarations. You can tell the annotation target by looking at the annotation. This reuse of the annotation location means that there is no need for new syntax for annotations on types in declarations.

Consider the following two field declarations.
  @NonNegative int balance;
  @GuardedBy("accessLock") long lastAccessedTime;
The annotation @NonNegative applies to the field type int, not to the whole variable declaration nor to the variable itself. The annotation @GuardedBy("accessLock") applies to the field.

As another example, in
    @Deprecated
    @NonNull Dimension getSize() { ... }
@Deprecated applies to the method and @NonNull applies to the return type. This is because Deprecated is meta-annotated with ElementType.METHOD, and NonNull is meta-annotated with ElementType.TYPE.

The meta-annotation is written by the author of the annotation, as in
    @Target({ElementType.METHOD, ...})
    public @interface Deprecated { ... }

    @Target(ElementType.TYPE)
    public @interface NonNull { ... }
Java 6 already requires the compiler to read and enforce the Target meta-annotation.

The compiler applies the annotation to every target that is consistent with its meta-annotation. This means that, for certain syntactic locations, which target (Java construct) is being annotated depends on the annotation, or an annotation might even be applied to two targets. The order of annotations is not used to disambiguate; @NonNull @Deprecated Dimension getSize() has the same meaning but is poor style. (An annotation processor could warn about this order, just as tools warn about modifiers --- such as final static --- that are not written in the order recommended by Sun.)

Different syntaxes are possible, in which declaration and type annotations appear in different locations in the grammar. Such a syntax is warranted in two circumstances. (1) If programmers find it confusing to determine which construct an annotation applies to, and the alternate syntax is clearer overall. (2) If there exist annotations that can apply equally well to both methods and return value types (or to both types and variable declarations, etc.), and that have different semantics in the two situations. Both circumstances are poor style, and we have not yet found examples of such annotations. Another argument for the alternate syntax is that the grammar should be maximally flexible to permit unforeseen future uses of such annotations. This must be traded off against readability and usability for important known common cases.

3.5  Syntax of array annotations

As discussed in Section 3.3, it is desirable to be able to independently annotate both the element type and each distinct level of a nested array. We have not yet settled on a syntax for such annotations, however; this section presents several proposals.

For the array syntax, there are two choices to make. First, where should array annotations appear? Second, should an annotation on a set of brackets refer to the array or the elements? Taking the within-the-brackets syntax as an example, would @NonNull Document[@Readonly] mean that the array is @Readonly and contains @NonNull elements, or that the array is @NonNull and contains @Readonly elements? (For the fully postfix syntax, the second question is moot: the only sensible choice is for the annotation on the brackets to refer to the array, not the elements.)

Here are some principles that an ideal syntax would satisfy.

P1
Adding array levels should not change the meaning of existing annotations. For example, it would be confusing to have a syntax in which
  @A List<@B Object>        // @A refers to List
  @A List<@B Object>[@C]    // @A refers to array, @C refers to List
Another way of stating this principle is that one part of a declaration should describe a type that is part of the declared type. Stating a subtype of the given type should not require shuffling around the annotations.

P2
When two variables appear in a variable declaration, the annotations should mean the same thing for both variables. In Java, arrays can be declared with brackets after the type, after the identifier, or both, as in String[] my2dArray[];. For example, arr1 should have the same annotations as the elements of arr2:
  @A T[@B] arr1, arr2[@C];
Likewise, the Ts should have the same annotations for v3 and arr4:
  @A T v3, arr4[@B][@C];
And, these three declarations should mean the same thing:
  @A T[@B] arr5[@C];
  @A T[@B][@C] arr6;
  @A T arr7[@B][@C];
P3
Type annotations before a declaration refer to the full type, just as variable annotations (which occur in the same position --- at the very beginning of the declaration) refer to the entire variable. This is also consistent with annotations on generics (though the syntax of generics and arrays is quite different in other ways), where @NonNull List<String> is a non-null List of possibly-null Strings. This principle is inconsistent with principles P1 and P2, unless type annotations are forbidden before a declaration.
If an annotation on brackets refers to the array, then the syntax violates principle P3. If an annotation on brackets refers to the elements, then the syntax violates principles P1 and P2.

Here are several proposals for the syntax of such array annotations.

The examples below use the following variables:
array_of_rodocs a mutable one-dimensional array of immutable Documents
roarray_of_docs an immutable one-dimensional array of mutable Documents
array_of_array_of_rodocs a mutable array, whose elements are mutable one-dimensional arrays of immutable Documents
array_of_roarray_of_docs an immutable array, whose elements are mutable one-dimensional arrays of mutable Documents
roarray_of_array_of_docs a mutable array, whose elements are immutable one-dimensional arrays of mutable Documents
  1. Within brackets, refer to the array being accessed

    An annotation before the entire array type binds to the member type that it abuts; @Readonly Document[][] can be interpreted as (@Readonly Document)[][].

    An annotation within brackets refers to the array that is accessed using those brackets.

    The type of elements of @A Object[@B][@C] is @A Object[@C].

    The example variables would be declared as follows:
        @Readonly Document[] array_of_rodocs;
        Document[@Readonly] roarray_of_docs;
        @Readonly Document[][] array_of_array_of_rodocs = new Document[2][12];
        Document[@Readonly][] array_of_roarray_of_docs = new Document[@Readonly 2][12];
        Document[][@Readonly] roarray_of_array_of_docs = new Document[2][@Readonly 12];
    
  2. Within brackets, refer to the elements being accessed

    An annotation before the entire array type refers to the (reference to the) top-level array itself; @Readonly Document[][] docs4 indicates that the array is non-modifiable (not that the Documents in it are non-modifiable).

    An annotation within brackets applies to the elements that are accessed using those brackets.

    The type of elements of @A Object[@B][@C] is @B Object[@C].

    The example variables would be declared as follows:
        Document[@Readonly] array_of_rodocs;
        @Readonly Document[] roarray_of_docs;
        Document[][@Readonly] array_of_array_of_rodocs = new Document[2][@Readonly 12];
        Document[@Readonly][] array_of_roarray_of_docs = new Document[@Readonly 2][12];
        @Readonly Document[][] roarray_of_array_of_docs = new Document[2][12];
    
  3. Outside brackets, prefix

    The type of elements of @A Object @B [] @C [] is @B Object @C [].

    The example variables would be declared as follows:
        Document @Readonly [] array_of_rodocs;
        @Readonly Document[] roarray_of_docs;
        @Readonly Document[][] array_of_array_of_rodocs = new Document[2][12];
        Document[] @Readonly [] array_of_roarray_of_docs = new Document[2] @Readonly [12];
        Document @Readonly [][] roarray_of_array_of_docs = new Document @Readonly [2][12];
    
  4. Outside brackets, postfix

    The type of elements of @A Object[] @B [] @C is @B Object[] @C.

    In Java, array types are constructed using postfix syntax, so postfix annotation syntax for them is appealing.

    Possible disadvantage: Prefix notation may be more natural to Java programmers, as it is used in other places in the Java syntax.

    The example variables would be declared as follows:
        Document[] @Readonly array_of_rodocs;
        @Readonly Document[] roarray_of_docs;
        Document[][] @Readonly array_of_array_of_rodocs = new Document[2][12] @Readonly;
        Document[] @Readonly [] array_of_roarray_of_docs = new Document[2] @Readonly [12];
        @Readonly Document[][] roarray_of_array_of_docs = new Document[2][12];
    
    or, in a fully postfix syntax:
        Document @Readonly [] array_of_rodocs;
        Document[] @Readonly roarray_of_docs;
        Document @Readonly [][] array_of_array_of_rodocs = new Document[2][12] @Readonly;
        Document[] @Readonly [] array_of_roarray_of_docs = new Document[2] @Readonly [12];
        Document[][] @Readonly roarray_of_array_of_docs = new Document[2][12];
    
The within-the-brackets syntax has problems with ambiguity. In this example the annotated element could be the array or the type Y:
  new X[@ReadOnly Y.class.getMethods().length]
And in this example, the annotated element is the array, but the annotation could be the marker annotation @ReadOnly with a parenthesized expression (2) or could be the annotation @ReadOnly(2).
  new X[2][@ReadOnly (2) ]
It is also possible to imagine array annotations that do not require new locations for the annotations. The advantage of this is that there is no new syntax. A disadvantage is that the array level annotations are syntactically separated from the array levels themselves, so the meaning may not be as clear.
  1. Use an array-valued annotation that gives the annotations for the different dimensions. It could give the dimensions explicitly:
       // dimension 1 and 2 of the array are annotated
       @ArrayAnnots({
         @ArrayAnnot(i=1, value={Readonly.class}),
         @ArrayAnnot(i=2, value={Readonly.class})
       })
       Object[][][] arr;
    
    or use the order in which the annotations are given.
       @ArrayAnnots({
         @ArrayAnnot({Readonly.class}),
         @ArrayAnnot({Readonly.class})
       })
       Object[][] arr2;
    
       @ArrayAnnots({
         @Readonly,
         @Readonly
       })
       Object[][] arr2;
    
    The latter syntax is less convenient when not every level of the array is being annotated, or when multiple annotations are put on an array. (This document should give examples of those situations.)

  2. Use an annotation that lists the dimensions that have a property:
       // In each case, the elements in the array are readonly
       // dimension 0 has no annotation
       // dimensions 1 and 2 are also readonly
    
       @ReadonlyDims({1,2}) @Readonly Object[][][] roa;
       @Dims({1,2}, @Readonly) @Readonly Object[][][] roa;
    
    One advantage of this syntax over the one that gives an array of annotations is that each annotation is given independently, so it will be easier for tools to insert, delete, or conditionally display a given annotation. However, the array of annotations more closely mirrors the syntax of the array declaration itself.

4  Class file format extensions

Java annotations (including the extended annotations) must be stored in the class file for two reasons. First, annotated signatures (public members) must be available to tools that read class files, such as a compiler (really, an annotation processor or type-checking plug-in [Dar06]) when compiling a client of the class file. Second, annotated method bodies must be present to permit verification of the correctness of the annotated signatures in the class files; this is necessary to give confidence in an entire system, since class files may originate from any source.

This document proposes conventions for storing the annotations described in Section 3, as well as for storing local variable annotations, which are permitted in Java syntax but currently discarded by the compiler. Class files already store annotations in the form of ``attributes'' [Bra04a, LY]. JVMs ignore unknown attributes. For backward compatibility, we use new attributes for storing the type annotations. In other words, our proposal merely reserves the names of a few attributes and specifies their layout. Our proposal does not alter the way that existing annotations on classes, methods, method parameters, and fields are stored in the class file. Class files generated from programs that use no new annotations will be identical to those generated by a standard Java SE 6 (that is, pre-extended-annotations) compiler. Furthermore, the bytecode array will be identical between two programs that differ only in their annotations. Attributes have no effect on the bytecode array, because they exist outside it; however, they can represent properties of it by referring to the bytecode (including specific instructions, or bytecode offsets).

In Java SE 6, annotations are stored in the class file in attributes of the classes, fields, or methods they target. Attributes are sections of the class file that associate data with a program element (a method's bytecodes, for instance, are stored in a Code attribute). The RuntimeVisibleAnnotationsattribute is used for annotations that are accessible at runtime using reflection, and the RuntimeInvisibleAnnotationsattribute is used for annotations that are not accessible at runtime. These attributes contain arrays of annotation structure elements, which in turn contain arrays of element_value pairs. The element_value pairs store the names and values of an annotation's arguments.

Our proposal introduces two new attributes: RuntimeVisibleTypeAnnotationsand RuntimeInvisibleTypeAnnotations. These attributes are structurally identical to the RuntimeVisibleAnnotationsand RuntimeInvisibleAnnotationsattributes described above with one exception: rather than an array of annotation elements, RuntimeVisibleTypeAnnotationsand RuntimeInvisibleTypeAnnotationscontain an array of extended_annotationelements, which are described in section 4.1 below.

The Runtime[In]visibleTypeAnnotations attributes store annotations written in the new locations described in Section 3, and on local variables. For annotations on the type of a field, the field_info structure (see JVMS3 §4.6) corresponding to that field stores the Runtime[In]visibleTypeAnnotations attributes. For annotations on types in method signatures or bodies, the method_info structure (see JVMS3 §4.7) that corresponds to the annotations' containing method stores the Runtime[In]visibleTypeAnnotations attributes. For annotations on class type parameter bounds and class extends/implements types, the attributes structure (see JVMS3 §4.2) stores the Runtime[In]visibleTypeAnnotations attributes.

4.1  The extended_annotationstructure

The extended_annotationstructure has the following format, which adds target_type and reference_info to the annotation structure defined in JVMS3 §4.8.15:
extended_annotation {
    u2 type_index;
    u2 num_element_value_pairs;
    {
        u2 element_name_index;
        element_value value;
    } element_value_pairs[num_element_value_pairs];
    u1 target_type;    // new in our proposal: where the annotation appears
    {
        ...
    } reference_info;  // new in our proposal: where the annotation appears
}
We briefly recap the fields of annotation, which are described in in JVMS3 §4.8.15. The following sections describe the fields of the extended_annotationstructure that differ from annotation.

4.1.1  The target_type field

The target_type field denotes the type of program element that the annotation targets. As described above, annotations in any of the following locations are written to Runtime[In]visibleTypeAnnotations attributes in the class file: The corresponding values for each of these cases are shown in Figure 2. Some locations are assigned numbers even though annotations in those locations are prohibited or are actually written to Runtime[In]visibleAnnotations or Runtime[In]visibleParameterAnnotations. While those locations will never appear in a target_type field, including them in the enumeration may be convenient for software that processes extended annotations. They are marked * in Figure 2.

Annotation Target target_type Value
typecast 0x00
typecast generic/array 0x01
type test (instanceof) 0x02
type test (instanceof) generic/array 0x03
object creation (new) 0x04
object creation (new) generic/array 0x05
method receiver 0x06
method receiver generic/array 0x07*
local variable 0x08
local variable generic/array 0x09
method return type 0x0A*
method return type generic/array 0x0B
method parameter 0x0C*
method parameter generic/array 0x0D
field 0x0E*
field generic/array 0x0F
class type parameter bound 0x10
class type parameter bound generic/array 0x11
method type parameter bound 0x12
method type parameter bound generic/array 0x13
class extends/implements 0x14
class extends/implements generic/array 0x15
exception type in throws 0x16
exception type in throws generic/array 0x17*

Figure 2: Values of target_type for each possible target of a type annotation. Enumeration elements marked * will never appear in a target_type field but are included for completeness and convenience for annotation processors. Ordinary Java annotations on declarations are not included, because they appear in annotation, not extended_annotation, attributes in the class file. Table elements such as local variable, method parameter, and field refer to the declaration, not the use, of such elements.
TODO: add to this table: generic type arguments in a generic method invocation; class literals.


4.1.2  The reference_info field

The reference_info field is used to reference the annotation's target in bytecode. The contents of the reference_info field is determined by the value of target_type.

Typecasts, type tests, and object creation
When the annotation's target is a typecast, an instanceof expression, or a new expression, reference_info has the following structure:
    {
        u2 offset;
    } reference_info;
The offset field denotes the offset (i.e., within the bytecodes of the containing method) of the checkcast bytecode emitted for the typecast, the instanceof bytecode emitted for the type tests, or of the new bytecode emitted for the object creation expression. Typecast annotations are attached to a single bytecode, not a bytecode range (or ranges): the annotation provides information about the type of a single value, not about the behavior of a code block. A similar argument applies to type tests and object creation.

For annotated typecasts, the attribute may be attached to a checkcast bytecode, or to any other bytecode. The rationale for this is that the Java compiler is permitted to omit checkcast bytecodes for typecasts that are guaranteed to be no-ops. For example, a cast from String to @NonNull String may be a no-op for the underlying Java type system (which sees a cast from String String). If the compiler omits the checkcast bytecode, the @NonNull attribute would be attached to the (last) bytecode that creates the target expression instead. This approach permits code generation for existing compilers to be unaffected.

See the end of this section for handling of generic type arguments and arrays.

Local Variables
When the annotation's target is a local variable, reference_info has the following structure:
    {
        u2 start_pc;
        u2 length;
        u2 index;
    } reference_info;
The start_pc and length fields specify the variable's live range in the bytecodes of the local variable's containing method (from offset start_pc to offset start_pc + length). The index field stores the local variable's index in that method. These fields are similar to those of the optional LocalVariableTable attribute defined in JVMS3 §4.8.13.

Storing local variable annotations in the class file raises certain challenges. For example, live ranges are not isomorphic to local variables. Further, a local variable with no live range may not appear in the class file (but it is also irrelevant to the program).

Method Receivers
When the annotation's target is a method receiver, reference_info is empty.

Type Parameter Bounds
When the annotation's target is a bound of a type parameter of a class or method, reference_info has the following structure:
    {
        u1 param_index;
        u1 bound_index;
    } reference_info;
param_index specifies the index of the type parameter, while bound_index specifies the index of the bound. Consider the following example:
    <T extends @A Object & @B Comparable, U extends @C Cloneable>
Here @A has param_index 0 and bound_index 0, @B has param_index 0 and bound_index 1, and @C has param_index 1 and bound_index 0.

Class extends and implements Clauses
When the annotation's target is a type in an extends or implements clause, reference_info has the following structure:
    {
        u1 type_index;
    } reference_info;
type_index specifies the index of the type in the clause: -1 (255) is used if the annotation is on the superclass type, and the value i is used if the annotation is on the ith superinterface type.

throws Clauses
When the annotation's target is a type in a throws clause, reference_info has the following structure:
    {
        u1 type_index;
    } reference_info
type_index specifies the index of the exception type in the clause: the value i denotes an annotation on the ith exception type.

Generic Type Arguments or Arrays
When the annotation's target is a generic type argument or array type, reference_info contains what it normally would for the raw type (e.g., offset for an annotation on a type argument in a typecast), plus the following fields at the end:
    u2 location_length;
    u1 location[location_length];
The location_length field specifies the number of elements in the variable-length location field. location encodes which type argument or array element the annotation targets. Specifically, the ith item in location denotes the index of the type argument or array dimension at the ith level of the hierarchy. Figure 3 shows the values of the location_length and location fields for the annotations in a sample field declaration.


Declaration: @A Map<@B Comparable<@C Object[@D][@E][@F]>, @G List<@H Document>>

 
Annotation location_length location
@A not applicable
@B 1 0
@C 2 0, 0
@D 3 0, 0, 0
@E 3 0, 0, 1
@F 3 0, 0, 2
@G 1 1
@H 2 1, 0

Figure 3: Values of the location_length and location fields for a sample declaration.


5  Required tool and specification modifications

This section indicates the tools and specifications that must be modified in order for the Java language and tools to support JSR 308. The implementation of extended annotations builds on the existing framework for Java annotations.

5.1  Compiler

The syntax extensions described in Section 3 require the javac Java compiler to accept annotations in the proposed locations and to add them to the program's AST. The relevant AST node classes must also be modified to store these annotations.

Javac's -Xprint functionality reads a .class file and prints the interface (class declarations with signatures of all fields and methods). This must be updated to print the extended annotations as well. (The -Xprint functionality is similar to javap, but cannot provide any information about bytecodes or method bodies, because it is implemented internally as an annotation processor.)

When creating bridge methods (an implementation strategy used when the erased signature of the actual method being invoked differs from that of the compile-time method declaration [GJSB05, §15.12.4.5]), annotations should be copied from the method being invoked. (Right now, javac doesn't copy/transfer any annotations from original methods to the bridge methods; that is probably a bug in javac.)

When generating .class files, the compiler must emit the attributes described in Section 4.

The compiler is required to preserve annotations in the class file. More precisely, if a programmer places an annotation (with class file or runtime retention) on the type of an expression, then the annotation must be present, in the compiled class file, on the type of the compiled representation of that expression. This may change the compiler implementation of certain optimizations, such as common subexpression elimination, but this restriction on the compiler implementation is unobjectionable for three reasons.
  1. Java-to-bytecode compilers rarely perform sophisticated optimizations, since the bytecode-to-native (JIT) compiler is the major determinant in Java program performance. Thus, the restriction will not affect most compilers.
  2. Second, the compiler workarounds are simple. Suppose that two expressions that are candidates for common subexpression elimination have different type annotations. A compiler could: not perform the optimization when the annotations differ; create a single expression whose type has both of the annotations (e.g., merging (@Positive Integer) 42 and (@Even Integer) 42 into (@Positive @Even Integer) 42); or create an unannotated expression and copy its value into two variables with differently-annotated types.
  3. It seems unlikely that two identical, non-trivial expressions would have differently-annotated types. Thus, any compiler restrictions will have little or no effect on most compiled programs.

5.2  Annotation processing

The Tree API, which exposes the AST (including annotations) to authors of annotation processors (compile-time plug-ins), must be updated to reflect the modifications made to the internal AST node classes described in Section 3.

The JSR 269 annotation processing API must be modified so that the process method (currently invoked only on class, field, and method annotations) is also invoked on annotations on every annotatable location.1

Annotation processors specified by the -processor compiler option run after class members are resolved but before method bodies are resolved. Resolution (also called ``attribution'') determines type information; thus, a JSR 269 annotation processor has access to the types of fields and method return and parameters, but not types for local variables and expressions, which a type-checking plug-in needs in order to check variable uses. We will add a new -typeprocessor compiler option that specifies an annotation processor that runs after resolution/attribution, and which can therefore depend on knowing the types of all expressions.

Like reflection, the JSR 269 (annotation processing) model does not represent constructs below the method level, such as individual statements and expressions. Therefore, it needs to be updated only with respect to annotations on class member declarations. The JSR 269 model, javax.lang.model.*, already has some classes representing annotations; see https://docs.oracle.com/javase/6/docs/api/javax/lang/model/element/package-summary.html. The annotation processing API in javax.annotation.processing must also be revised.

The specification of ElementType.TYPE in java.lang.annotation.ElementType must be revised to permit annotations meta-annotated with ElementType.TYPE to appear on any use of a type, not just on declarations.

5.3  Reflection

The java.lang.reflect.* and java.lang.Class APIs give access to annotations on public API elements such as classes, method signatures, etc. They must be updated to give the same access to the new extended annotations.

For example, to parallel the existing Method.getAnnotations (for the return value) and Method.getParameterAnnotations (for the formal parameters), we would add Method.getReceiverAnnotation (for the receiver this). Reflection gives no access to method implementations, so we will not provide access to annotations on casts (or other annotations inside a method body), type parameter names, or similar implementation details.

Suppose that a method is declared as:
  @NonEmpty List<@Interned String> foo(@NonNull List<@Opened File> files) @Readonly {...}
Then Method.getAnnotations() returns the @NonEmpty annotation, just as in Java SE 6, and likewise Method.getParameterAnnotations() returns the @NonNull annotation. New method Method.getReceiverAnnotations() returns the @Readonly annotation. We have not yet decided how to provide reflective access to annotations on generic types in a method's signature, such as the instances of @Interned and @Opened above.

The Mirror API com.sun.mirror.* need not be updated, as it has been superseded by JSR 269 [Dar06].

5.4  Virtual machine and other tools that manipulate class files

No modifications to the virtual machine are necessary.

The javap disassembler must be updated to recognize the new class file format and to output annotations.

The pack200/unpack200 tool should preserve the new attributes through a compress-decompress cycle.

5.5  Other tools

Javadoc must output annotations at the new locations when those are part of the public API, such as in a method signature.

Similar modifications need to be made to tools outside the Sun JDK, such as IDEs (Eclipse, IDEA, JBuilder, jEdit, NetBeans), other tools that manipulate Java code (grammars for CUP, javacc), and tools that manipulate class files (ASM, BCEL). These changes need to be made by the authors of the respective tools.

A separate document, ``Custom type qualifiers via annotations on Java types'' (https://checkerframework.org/jsr308/java-type-qualifiers.pdf), explores implementation strategies for annotation processors that act as type-checking compiler plug-ins. It is not germane to this proposal, both because this proposal does not concern itself with annotation semantics and because writing such plug-ins does not require any changes beyond those described here.

A separate document, ``Annotation File Specification'' (https://checkerframework.org/jsr308/annotation-file-format.pdf), describes a textual format for annotations that is independent of .java or .class files. This textual format can represent annotations for libraries that cannot or should not be modified. We have built tools for manipulating annotations, including extracting annotations from and inserting annotations in .java and .class files. That file format is not part of this proposal for extending Java's annotations; it is better viewed as an implementation detail of our tools.

5.6  Java Language Specification

The Java Language Specification needs to be updated. A separate document will one day contain a list of all the changes. (The list of changes would be too long to include in this document, and would not succinctly convey the implications of the changes.) Finding all the places that mention annotations is a good start.

One nonobvious place is in places like section 9.6.1.5, where the description of @codeSuppressWarnings states ``If a program declaration is annotated ...'' and the use of ``declaration'' must be changed to ``element'' or ``construct'' or some similar word.

5.7  Java Virtual Machine Specification

The Java Virtual Machine Specification (JVMS) needs to be updated to describe the Runtime{Inv,V}isibleTypeAnnotations attributes. This section, or a separate document, will one day contain a list of all the changes. Since the third edition of JVMS [LY] has not yet been published, the changes must work from the document titled ``revisions to `The class file Format' '', which this document calls ``JVMS3'' and is available at https://docs.oracle.com/javase/specs/jvms/se5.0/ClassFileFormat-Java5.pdf.

6  Testing (TCK, Technology Compatibility Kit)

The JSR will ship with a test suite (known as a TCK, or Technology Compatibility Kit).

Each tool that needs to be tested appears in Section 5; the TCK will include tests for each of them.

For each modified tool, we will test backward compatibility by passing all of its existing tests. (We may need to modify a few of them, for instance those that depend on specific bytecodes that are created by the compiler.)

We will test most other functionality by creating a set of Java programs that include annotations in every possible location. For instance, this can be used to test all aspects of the compiler (parsing, code generation, -Xprint).

We will provide multiple annotation processors (including at least one for checking @NonNull and one for checking @Interned) that utilize the new annotations, along with a test suite for each one. Each annotation processor's test suite consists of annotated code, along with expected output from the given annotation processor. Since the annotation processors utilize all aspects of our changes, this serves as an additional end-to-end test of the JSR 308 implementation. As a side benefit, the annotation processors will be useful in their own right, will thereby illustrate the utility of JSR 308, and will serve as examples for people who wish to create their own type-checking plug-ins.

7  Other annotations

The Expert Group will consider whether the proposal should extend annotations in a few other ways that are not directly related to annotations on types. This is especially true if the additional changes are small, that there is no better time to add such an annotation, and the new syntax would permit unanticipated future uses. Two examples follow, for which the proposal does not currently include a detailed design.

7.1  Duplicate annotations at a location

Currently, array-valued annotations can be clumsy to write:
@Resources({
    @Resource(name = "db1", type = DataSource.class)
    @Resource(name = "db2", type = DataSource.class)
})
public class MyClass { ... }
Likewise, it may be desirable for some (but not all) annotations to be specified more than once at a single location. A cleaner syntax like
@Resource(name = "db1", type = DataSource.class)
@Resource(name = "db2", type = DataSource.class)
public class MyClass { ... }
may be desirable for both purposes.

7.2  Annotations on statements

Java does not currently permit annotations on statements. Annotations on statements (or on some subset of statements, such as blocks or loops) could be useful for properties such as atomicity/concurrency. Such an extension would require defining both Java syntax and a convention for storing the information in the class file.

8  Logistical matters

The JSR for annotations on Java types should be included under the Java SE 7 umbrella JSR (which lists the JSRs that are part of the Java SE 7 release). However, it should be a separate JSR because it needs a separate expert group. The expert group will have overlap with any others dealing with other added language features that might be annotatable (such as method-reference types or closures), to check impact.

The specification and the TCK will be freely available, most likely licensed under terms that permit arbitrary use. The prototype implementation is built on the OpenJDK Java implementation and is publicly available; our goal is to have our changes incorporated into the official OpenJDK release.

To ease the transition from standard Java SE 6 code to code with the extended annotations, the prototype implementation recognizes the extended annotations when surrounded by comment markers:
  /*@Readonly*/ Object x;
This permits use of both standard Java SE 6 tools and the new annotations even before Java SE 7 is released. However, it is not part of the proposal, and the final Java SE 7 implementation will not recognize the new annotations when embedded in comments. The Spec# [BLS04] extension to C# can be made compilable by a standard C# compiler in a similar way, by enclosing its annotations in special /*^...\^*/ comment markers. The /*@ comment syntax is a standard part of the Splint [Eva96] and JML [LBR06] tools (that is, not with the goal of backward compatibility).

9  Out-of-scope issues

This section of the document discusses several issues that are not in scope for JSR 308.

The last annotations JSR.
It is not a goal that JSR 308 is the last annotation-related JSR. It is acceptable to leave some issues to future language designers, just as JSR 175 (the previous annotations JSR [Bra04a]) did. It is a goal not to unnecessarily close off realistic future avenues of extension.

9.1  Locations for annotations

Expression annotations.
Annotating a type cast indicates a property of a value (the result of an expression). This is different than annotating the expression itself, which indicates some property of the entire computation, such as that it should be performed atomically, that it acquires no locks, or that it should be formatted specially by an IDE. JSR 308 does not support expression annotations, because we have not yet discovered compelling use cases for them that cannot be equally well supported by statement annotations. (A minor inconvenience is that the use of statement annotations may require the programmer to create a separate statement for the expression to be annotated.)

Implicit Java types in casts.
Arbitrary values can be annotated using an annotation on a cast:
  (@Language("SQL") String) "select * from foo"
A possible shorthand would be to permit the Java type to be implicit:
  (@Language("SQL")) "select * from foo"
This is not permitted (nor may a cast be omitted in a type test, as in @codex instanceof @NonNull), for several reasons. Erasing the annotations should leave a valid Java program. Stating the type reinforces that the annotation is a type annotation rather than an expression annotation. The benefit of omitting the type in the cast seems relatively minor. Especially in a type test, stating the type reinforces that the run-time effect has is to check and change the Java type; no run-time check of the annotation is possible in general.

An even shorter shorthand would drop the parentheses:
  @Language("SQL") "select * from foo"
In addition to the benefits and problems noted above, such an annotation is syntactically ambiguous with an expression annotation. Whether an annotation applies to expressions or to types is clear from the annotation's documentation and its @Target meta-annotation, similarly to how it is determined whether an annotation applies to a type or to a declaration (Section 3.4). But a problem remains. If a within-brackets proposal for arrays (Section 3.5 is chosen, then Object[@X 2] might mean that the array level has annotation X or that it's shorthand for Object[(@X int) 2]; similar confusion might occur when the array length is a more complex expression.

Only certain statements.
It would be possible to permit annotations only on blocks and/or loops, as a restricted special case of statements. This is less general than permitting annotations on statements, and uses are more syntactically cluttered (for instance, this requires a statement to be converted into a block before it can be annotated). Most declarations could not be annotated as statements because enclosing the declaration in a block to annotate it would change (and limit) the variable's scope. This limitation in flexibility does yield the advantage that there would be no syntactic ambiguity between (say) statement annotations and declaration or type annotations.

Similarly, permitting annotations on partial constructs (such as only the body of a loop) appears both more complex, and no more useful, than annotating complete constructs (such as a full statement).

9.2  Changes to the annotation type

Subclassing annotations.
Annotations cannot subclass one another, so it is difficult to share behavior or to express similarities or relationships among annotation types. (A meta-annotation can be used to work around this, but it is clumsy and indirect.)

Annotations as arguments to annotations
In Java, it is not possible to define an annotation that takes an arbitrary annotation as a parameter, as in
  @DefaultAnnotation(@MyAnnotation)
More generally, annotation types cannot have members of their own type. (An annotation whose parameter is an annotation of a specific type is explicitly permitted (JLS §9.6 and §9.7).) These limitations reduce the expressiveness of annotations, for instance making it impossible to define the @DefaultAnnotation above.

Positional arguments
Annotation types cannot have positional arguments (except for the value argument, when it is the only argument). This limitation makes writing annotations with multiple arguments more verbose than necessary.

9.3  Semantics of annotations

Annotations for specific purposes.
JSR 308 does not define any annotations nor take any position on their semantics. JSR 308 extends the Java and class file syntax to permit annotations to be written in more places, and thus makes existing and future annotations more useful to programmers.

By contrast, JSR 305 ``Annotations for Software Defect Detection'' aims to define a set of annotations for specific purposes, along with their semantics. Examples include type annotations such as non-nullness (@Nonnull), signedness (@Nonnegative), tainting, and string format; and also non-type annotations such as whether a method's return value should always be checked by the caller. For more details, see https://jcp.org/en/jsr/detail?id=305 and http://groups.google.com/group/jsr-305/.

Annotation inheritance.
The annotation type java.lang.annotation.Inherited (JLS §9.6.1.3) indicates that annotations on a class C corresponding to a given annotation type are inherited by subclasses of C. This implies that annotations on interfaces are not inherited, nor are annotations on members (methods, constructors, fields, etc.). It might be useful to provide a more fine-grained mechanism that applies different rules to classes, methods, fields, etc., or even to specify inheritance of annotations from interfaces. These semantic issue are out of the scope of JSR 308 but may be taken up by JSR 305 (``Annotations for Software Defect Detection'' [Pug06]).

Default annotations.
Specifying a default for annotations can reduce code size and (when used carefully and sparingly) increase code readability. For instance, Figure 1 uses @NonNullDefault to avoid the clutter of 5 @NonNull annotations. It would be nicer to have a general mechanism, such as
  @DefaultAnnotation(NonNull.class, locations={ElementType.LOCAL_VARIABLE})
Defaults for annotations are a semantic issue that is out of the scope of JSR 308. It will be taken up by JSR 305 (``Annotations for Software Defect Detection'' [Pug06]).

The defaulting syntax must also be able to specify the arguments to the default annotation (in the above example, the arguments to @NonNull).

A better syntax would use an annotation, not a class literal, as the argument to @DefaultAnnotation, as in
  @DefaultAnnotation(@MyAnnotation(arg="foo"))
but in Java, it is not possible to define an annotation that takes an arbitrary annotation as a parameter; see Section 9.2.

An issue for JSR 260 (Javadoc) and JSR 305 (Annotation semantics) is how inherited and defaulted annotations are handled in Javadoc: whether they are written out in full, or in some abbreviated form. Just as too many annotations may clutter source code, similar clutter-reduction ideas may need to be applied to Javadoc.

9.4  Type abbreviations and typedefs

An annotated type may be long and hard to read; compare Map<String, Object> to @NonNull Map<@NonNull String, @NonNull Object>. Class inheritance annotations and subclassing provides a partial solution, as noted in Section 3.3 with the following example:
  final class MyStringMap extends
    @Readonly Map<@NonNull String, @NonEmpty List<@NonNull @Readonly String>> {}
This approach limits reusability: if a method is declared to take a MyStringMap parameter, then a Map (even of the right type, including annotations) cannot be passed to it. (By contrast, a MyStringMap can always be used where a Map of the appropriate type is expected.) Goetz [Goe06] recommends exploiting Java's type inference to avoid some (but not all) instances of the long type name.

In summary, a built-in typedef mechanism might increase code readability.

9.5  Class file syntax

Changes to the class file syntax are out of the scope of JSR 308, which, for backward compatibility, does not change the way that existing annotations are stored in the class file.

However, some changes to the class file syntax have significant benefits, and could be the subject of another, small, JSR whose focus is only the class file format. Class file syntax changes require modification of compilers, JVMs, javap, and other class file tools (see Sections 5.4 and 5.5).

Reducing class file size via use of the constant pool.
Annotations could be stored in the constant pool, and use constant pool references from the annotation points? That would reduce class file size, especially if an annotation is used in many places in the same class, as is more likely with the annotations enabled by JSR 308 and those proposed in JSR 305.

10  Related work

Section 2.1 gave many examples of how type qualifiers have been used in the past.

C#'s attributes [ECM06, chap. 24] play the same role as Java's annotations: they attach metadata to specific parts of a program, and are carried through to the compiled bytecode representation, where they can be accessed via reflection. The syntax is different: C# uses [AnnotationName] or [AnnotationName: data] where Java uses @AnnotationName or @AnnotationName(data); C# uses AttributeUsageAttribute where Java uses Target; and so forth. However, C# permits metadata on generic arguments, and C# permits multiple metadata instances of the same type to appear at a given location.

Like Java, C# does not permit metadata on elements within a method body. (The ``[a]C#'' language [CCC05], whose name is pronounced ``annotated C sharp'', is an extension to C# that permits annotation of statements and code blocks.)

Harmon and Klefstad [HK07] propose a standard for worst-case execution time annotations.

Pechtchanski's dissertation [Pec03] uses annotations in the aid of dynamic program optimization. Pechtchanski implemented an extension to the Jikes compiler that supports stylized comments, and uses these annotations on classes, fields, methods, formals, local variable declarations, object creation (new) expressions, method invocations (calls), and program points (empty statements). The annotations are propagated by the compiler to the class file.

Mathias Ricken's LAPT-javac (https://ricken.us/research/laptjavac/) is a version of javac (version 1.5.0_06) that encodes annotations on local variables in the class file, in new Runtime{Inv,V}isibleLocalVariableAnnotations attributes. The class file format of LAPT-javac differs from that proposed in this document.

The Java Modeling Language, JML [LBR06], is a behavioral modeling language for writing specifications for Java code. It uses stylized comments as annotations, some of which apply to types.

Ownership types [CPN98, Boy04, Cla01, CD02, PNCB06, NVP98, DM05, LM04, LP06] permit programmers to control aliasing and access among objects. Ownership types can be expressed with type annotations and have been applied to program verification [LM04, Mül02, MPHL06], thread synchronization [BLR02, JPLS05], memory management [ACG+06, BSBR03], and representation independence [BN02].

JavaCOP [ANMM06] is a framework for implementing pluggable type systems in Java. Unlike JSR 308, JavaCOP does not use standard interfaces such as the Tree API and the JSR 269 annotation processing framework. JavaCOP provides a declarative pattern-matching and rule-based language; a type checker must be programmed in a combination of this language and in Java. JavaCOP's authors have defined over a dozen type-checkers in their language, but they do not report having run any of these type-checkers on a program to verify that the program satisfies the pluggable type system. As of this writing, no implementation is publicly available.

Acknowledgments

Matt Papi designed and implemented the JSR 308 compiler as modifications to Sun's javac compiler, and contributed to the JSR 308 design.

The members of the JSR 308 mailing list (https://types.cs.washington.edu/list-archives/jsr308/) provided valuable comments and suggestions. We welcome additional feedback.

At the 5th annual JCP Program Awards (in May 2007), JSR 308 received the Most Innovative Java SE/EE JSR of the Year award.

References

[AAA06]
Marwan Abi-Antoun and Jonathan Aldrich. Bringing ownership domains to mainstream Java. In Companion to Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2006), pages 702--703, Portland, OR, USA, October 24--26, 2006.

[ACG+06]
Chris Andrea, Yvonne Coady, Celina Gibbs, James Noble, Jan Vitek, and Tian Zhao. Scoped types and aspects for real-time systems. In ECOOP 2006 --- Object-Oriented Programming, 20th European Conference, pages 124--147, Nantes, France, July 5--7, 2006.

[AFKT03]
Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi. Checking and inferring local non-aliasing. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pages 129--140, San Diego, CA, USA, June 9--11, 2003.

[ANMM06]
Chris Andreae, James Noble, Shane Markstrum, and Todd Millstein. A framework for implementing pluggable type systems. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2006), pages 57--74, Portland, OR, USA, October 24--26, 2006.

[BE04]
Adrian Birka and Michael D. Ernst. A practical type system and language for reference immutability. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2004), pages 35--49, Vancouver, BC, Canada, October 26--28, 2004.

[BLR02]
Chandrasekhar Boyapati, Robert Lee, and Martin Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2002), pages 211--230, Seattle, WA, USA, October 28--30, 2002.

[BLS04]
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 49--69, Marseille, France, March 10--13, 2004.

[BN02]
Anindya Banerjee and David A. Naumann. Representation independence, confinement, and access control. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 166--177, Portland, Oregon, January 16--18, 2002.

[Boy04]
Chandrasekhar Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, MIT Department of Electrical Engineering and Computer Science, Cambridge, MA, February 2004.

[Bra04a]
Gilad Bracha. JSR 175: A metadata facility for the Java programming language. https://jcp.org/en/jsr/detail?id=175, September 30, 2004.

[Bra04b]
Gilad Bracha. Pluggable type systems. In OOPSLA Workshop on Revival of Dynamic Languages, Vancouver, BC, Canada, October 2004.

[BSBR03]
Chandrasekhar Boyapati, Alexandru Salcianu, William Beebee, Jr., and Martin Rinard. Ownership types for safe region-based memory management in real-time java. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pages 324--337, San Diego, CA, USA, June 9--11, 2003.

[CCC05]
Walter Cazzola, Antonio Cisternino, and Diego Colombo. Freely annotating C#. Journal of Object Technology, 4(10):31--48, December 2005. Special Issue: OOPS Track at SAC 2005.

[CD02]
Dave Clarke and Sophia Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2002), pages 292--310, Seattle, WA, USA, October 28--30, 2002.

[Cla01]
David Clarke. Object Ownership and Containment. PhD thesis, University of New South Wales, Sydney, Australia, 2001.

[CMM05]
Brian Chin, Shane Markstrum, and Todd Millstein. Semantic type qualifiers. In Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pages 85--95, Chicago, IL, USA, June 13--15, 2005.

[CPN98]
David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '98), pages 48--64, Vancouver, BC, Canada, October 20--22, 1998.

[Dar06]
Joe Darcy. JSR 269: Pluggable annotation processing API. https://jcp.org/en/jsr/detail?id=269, May 17, 2006. Public review version.

[Det96]
David L. Detlefs. An overview of the Extended Static Checking system. In Proceedings of the First Workshop on Formal Methods in Software Practice, pages 1--9, January 1996.

[DF01]
Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, pages 59--69, Snowbird, UT, USA, June 20--22, 2001.

[DLNS98]
David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, December 18, 1998.

[DM05]
Werner Dietl and Peter Müller. Universes: Lightweight ownership for JML. Journal of Object Technology (JOT), 4(8):5--32, October 2005.

[EC06]
Michael D. Ernst and Danny Coward. JSR 308: Annotations on Java types. https://checkerframework.org/jsr308/, October 17, 2006.

[ECM06]
Ecma 334: C# language specification, 4th edition. ECMA International, June 2006.

[EFA99]
Martin Elsman, Jeffrey S. Foster, and Alexander Aiken. Carillon --- A System to Find Y2K Problems in C Programs, July 30, 1999.

[Eva96]
David Evans. Static detection of dynamic memory errors. In Proceedings of the SIGPLAN '96 Conference on Programming Language Design and Implementation, pages 44--53, Philadelphia, PA, USA, May 21--24, 1996.

[FL03]
Manuel Fähndrich and K. Rustan M. Leino. Declaring and checking non-null types in an object-oriented language. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2003), pages 302--312, Anaheim, CA, USA, November 6--8, 2003.

[FTA02]
Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pages 1--12, Berlin, Germany, June 17--19, 2002.

[GF05]
David Greenfieldboyce and Jeffrey S. Foster. Type qualifiers for Java. http://www.cs.umd.edu/Grad/scholarlypapers/papers/greenfiledboyce.pdf, August 8, 2005.

[GJSB05]
James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification. Addison Wesley, Boston, MA, third edition, 2005.

[Goe06]
Brian Goetz. The pseudo-typedef antipattern: Extension is not type definition. https://web.archive.org/web/20170206190605/https://www.ibm.com/developerworks/java/library/j-jtp02216/index.html, February 21, 2006.

[HK07]
Trevor Harmon and Raymond Klefstad. Toward a unified standard for worst-case execution time annotations in real-time Java. In WPDRTS 2007, Fifteenth International Workshop on Parallel and Distributed Real-Time Systems, Long Beach, CA, USA, March 2007.

[JPLS05]
Bart Jacobs, Frank Piessens, K. Rustan M. Leino, and Wolfram Schulte. Safe concurrency for aggregate objects with invariants. In Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, pages 137--147, Koblenz, Germany, September 7--9, 2005.

[JW04]
Rob Johnson and David Wagner. Finding user/kernel pointer bugs with type inference. In 13th USENIX Security Symposium, pages 119--134, San Diego, CA, USA, August 11--13, 2004.

[KT01]
Günter Kniesel and Dirk Theisen. JAC --- access right based encapsulation for Java. Software: Practice and Experience, 31(6):555--576, 2001.

[LBR06]
Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes, 31(3), March 2006.

[LM04]
K. Rustan M. Leino and Peter Müller. Object invariants in dynamic contexts. In ECOOP 2004 --- Object-Oriented Programming, 18th European Conference, pages 491--, Oslo, Norway, June 16--18, 2004.

[LP06]
Yi Lu and John Potter. Protecting representation with effect encapsulation. In Proceedings of the 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 359--371, Charleston, SC, USA, January 11--13, 2006.

[LY]
Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. 3rd edition. To appear.

[Mor06]
Rajiv Mordani. JSR 250: Common annotations for the Java platform. https://jcp.org/en/jsr/detail?id=250, May 11, 2006.

[MPHL06]
Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular invariants for layered object structures. Science of Computer Programming, 62:253--286, October 2006.

[Mül02]
Peter Müller. Modular Specification and Verification of Object-Oriented Programs. Number 2262 in Lecture Notes in Computer Science. Springer-Verlag, 2002.

[NVP98]
James Noble, Jan Vitek, and John Potter. Flexible alias protection. In ECOOP '98, the 12th European Conference on Object-Oriented Programming, pages 158--185, Brussels, Belgium, July 20-24, 1998.

[PBKM00]
Sara Porat, Marina Biberstein, Larry Koved, and Bilba Mendelson. Automatic detection of immutable fields in Java. In CASCON, Mississauga, Ontario, Canada, November 13--16, 2000.

[Pec03]
Igor Pechtchanski. A Framework for Optimistic Program Optimization. PhD thesis, New York University, September 2003.

[Pfe92]
Frank Pfenning. Dependent types in logic programming. In Frank Pfenning, editor, Types in Logic Programming, chapter 10, pages 285--311. MIT Press, Cambridge, MA, 1992.

[PNCB06]
Alex Potanin, James Noble, Dave Clarke, and Robert Biddle. Generic ownership for generic Java. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2006), pages 311--324, Portland, OR, USA, October 24--26, 2006.

[PØ95]
Jens Palsberg and Peter Ørbæk. Trust in the l-calculus. In Proceedings of the Second International Symposium on Static Analysis, SAS '95, pages 314--329, Glasgow, UK, September 25--27, 1995.

[Pug06]
William Pugh. JSR 305: Annotations for software defect detection. https://jcp.org/en/jsr/detail?id=305, August 29, 2006. JSR Review Ballot version.

[STFW01]
Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format string vulnerabilities with type qualifiers. In 10th USENIX Security Symposium, Washington, DC, USA, August 15--17, 2001.

[SW01]
Mats Skoglund and Tobias Wrigstad. A mode system for read-only references in Java. In FTfJP'2001: 3rd Workshop on Formal Techniques for Java-like Programs, Glasgow, Scotland, June 18, 2001.

[TE05]
Matthew S. Tschantz and Michael D. Ernst. Javari: Adding reference immutability to Java. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2005), pages 211--230, San Diego, CA, USA, October 18--20, 2005.

[VS97]
Dennis M. Volpano and Geoffrey Smith. A type-based approach to program security. In TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, pages 607--621, Lille, France, April 14--18, 1997.

[Xi98]
Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, December 1998.

[XP99]
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 214--227, San Antonio, TX, January 20--22 1999.

[YSP+98]
Kathy Yelick, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, Paul Hilfinger, Susan Graham, David Gay, Phil Colella, and Alex Aiken. Titanium: A high-performance Java dialect. Concurrency: Practice and Experience, 10(11--13):825--836, September--November 1998.

1
JSR 269 is insufficient for a type-checking compiler plug-in (annotation processor), which must check at each use of a variable/method whose declaration is annotated. For example, if a variable x is declared as @NonNull Object x;, then every assignment to x must be checked, because any assignment x = null; would be illegal. Therefore, the prototype implementation of type-checking compiler plug-ins uses the Tree API to examine all of a class's code. Nonetheless, it may be desirable to extend JSR 269 to process all annotations, for consistency and to support other types of annotation processors.

This document was translated from LATEX by HEVEA.