Annotations on Java types

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

Contents:

• 1   Introduction
• 2   Example use of type annotations: Type qualifiers
  • 2.1   Examples of type qualifiers
• 3   Java language syntax extensions
  • 3.1   Source locations for annotations on types
  • 3.2   Examples of annotation syntax
  • 3.3   Uses of annotations on types
  • 3.4   Disambiguating type and declaration annotations
  • 3.5   Syntax of array annotations
• 4   Class file format extensions
  • 4.1   The extended_annotationstructure
    • 4.1.1   The target_type field
    • 4.1.2   The reference_info field
• 5   Required tool and specification modifications
  • 5.1   Compiler
  • 5.2   Annotation processing
  • 5.3   Reflection
  • 5.4   Virtual machine and other tools that manipulate class files
  • 5.5   Other tools
  • 5.6   Java Language Specification
  • 5.7   Java Virtual Machine Specification
• 6   Testing (TCK, Technology Compatibility Kit)
• 7   Other annotations
  • 7.1   Duplicate annotations at a location
  • 7.2   Annotations on statements
• 8   Logistical matters
• 9   Out-of-scope issues
  • 9.1   Locations for annotations
  • 9.2   Changes to the annotation type
  • 9.3   Semantics of annotations
  • 9.4   Type abbreviations and typedefs
  • 9.5   Class file syntax
• 10   Related work

1  Introduction

2  Example use of type annotations: Type qualifiers

2.1  Examples 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 ==.

---

3  Java language syntax extensions

3.1  Source locations for annotations on types

3.2  Examples of annotation syntax

• for generic type arguments to parameterized classes:

      Map<@NonNull String, @NonEmpty List<@Readonly Document>> files;
  

  
  
  
• for generic type arguments in a generic method or constructor invocation:

      o.<@NonNull String>m("...");
  

  
  
  
• for type parameter bounds and wildcards:

      class Folder<F extends @Existing File> { ... }
      Collection<? super @Existing File>
  

  
  
  
• for class inheritance:

      class UnmodifiableList<T> implements @Readonly List<@Readonly T> { ... }
  

  
  
  
• for throws clauses:

      void monitorTemperature() throws @Critical TemperatureException { ... }
  

  
  
  
• for typecasts:

      myString = (@NonNull String) myObject;
  

  It is not permitted to omit the Java type, as in myString = (@NonNull) myObject;; see Sections 3.3 and 9.1.
  
  
• for type tests:

      boolean isNonNull = myString instanceof @NonNull String;
  

  It is not permitted to omit the Java type, as in myString instanceof @NonNull; see Sections 3.3 and 9.1.
  
  
• for object creation:

      new @NonEmpty @Readonly List<String>(myNonEmptyStringSet)
  

  For generic constructors (JLS §8.8.4), the annotation follows the explicit type arguments (JLS §15.9):

      new <String> @Interned MyObject()
  

  
  
  
• for method receivers:

      public String toString() @Readonly { ... }
      public void write() @Writable throws IOException { ... }
  

  A method can express constraints on the generic parameters of the receiver (just as is possible for other formal parameters, albeit with a slightly different syntax):

      public int size() @Readonly<@Readonly> { ... }
      public void requiresNonNullKeys() <@NonNull,> { ... }
  

  
  
  
• for class literals:

      Class<@NonNull String> c = @NonNull String.class;
  

  
  
  
• for static member access:

      @NonNull Type.field
  

  
  
  
• for arrays:

      Document[@Readonly][] docs4 = new Document[@Readonly 2][12];
      Document[][@Readonly] docs5 = new Document[2][@Readonly 12];
  

  This syntax permits independent annotations for each distinct level of array, and for the elements; see Section 3.5 for alternative syntaxes.

3.3  Uses of annotations on types

• Annotations on generic type arguments and arrays are necessary so the programmer can fully specify types. Generic collection classes are declared one level at a time, so it is easy to annotate each level individually. It is desirable that the syntax for arrays be equally expressive, for uniformity.
  
  Here are examples of uses for annotations on array levels:
  • The Titanium [YSP⁺98] dialect of Java requires the ability to place the local annotation (indicating that a memory reference in a parallel system refers to data on the same processor) on various levels of an array, not just at the top level.
  • In a dependent type system [Pfe92, Xi98, XP99], one wishes to specify the dimensions of an array type, such as Object[@Length(3)][@Length(10)] for a 3×10 array.
  • An immutability type system, as discussed in Section 2.1, needs to be able to specify which levels of an array may be modified. Consider specifying a procedure that inverts a matrix in place. The procedure parameter type should guarantee that the procedure does not change the shape of the array (does not replace any of the rows with another row of a different length), but must permit changing elements of the inner arrays. In other words, the top-level array is immutable, the inner arrays are mutable, and their elements are immutable.
  • An ownership domain system [AAA06] uses array annotations to indicate properties of array parameters, similarly to type parameters.
  
  
  
• Method receivers (this) are formal parameters and thus are an implicit mention of a type. For example, the method PrintStream.println(String) has two formal parameters (and at run time, its invocation involves two actual arguments). In Java's syntax, one of the formal parameters (the receiver) is implicit, but for consistency and expressiveness the implicit use of the receiver type should be annotatable just as the explicit parameters are. Such annotations require new syntax to distinguish them from annotations on the return value.
  
  For example, this receiver annotation

    Dimension getSize() @Readonly { ... }
  

  indicates that getSize does not modify its receiver. This is different than saying the method has no side effects at all, so it is not appropriate as a method annotation (such as JML's pure annotation). This is also different than saying that a client should not modify the return value, so it is not appropriate as a return value annotation.
  
  As with annotations on formal parameters (which are already permitted by Java), annotations on the receiver do not affect the Java signature, compile-time resolution of overloading, or run-time resolution of overriding. The Java type of every receiver in a class is the same --- but their annotations, and thus their qualified type in a type qualifier framework, may differ.
  
  
• There are two distinct reasons to annotate the type in a type cast: to fully specify the casted type (including annotations that are retained without change), or to indicate an application-specific invariant that is beyond the reasoning capability of the Java type system. Because a user can apply a type cast to any expression, a user can annotate the type of any expression. (This is different than annotating the expression itself; see Section 9.1.)
  1. Annotations on type casts permit the type in a type cast to be fully specified, including any appropriate annotations. In this case, the annotation on the cast is the same as the annotation on the type of the operand expression. The annotations are preserved, not changed, by the cast, and the annotation serves as a reminder of the type of the cast expression. For example, in

       @Readonly Object x;
       ... (@Readonly Date) x ...
     

     the cast preserves the annotation part of the type and changes only the Java type. If a cast could not be annotated, then a cast would remove the annotation:

       @Readonly Object x;
       ... (Date) x ...              // annotation processor error due to casting away @Readonly
     

     This cast changes the annotation; it uses x as a non-@Readonly object, which changes its type and would require a run-time mechanism to enforce type safety.
     
     An annotation processor could permit the unannotated cast syntax but implicitly add the annotation, treating the cast type as @Readonly Date. This has the advantage of brevity, but the disadvantage of being less explicit and of interfering somewhat with the second use of cast annotations. Experience will indicate which design is better in practice.
     
     
  2. A second use for annotations on type casts is --- like ordinary Java casts --- to provide the compiler with information that is beyond the ability of its typing rules. Such properties are often called ``application invariants'', since they are facts guaranteed by the logic of the application program.
     
     As a trivial example, the following cast changes the annotation but is guaranteed to be safe at run time:

       final Object x = new Object();
       ... (@NonNull Object) x ...
     

     An annotation processing tool could trust such type casts, perhaps issuing a warning to remind users to verify their safety by hand or in some other manner. An alternative approach would be to check the type cast dynamically, as Java casts are, but we do not endorse such an approach, because annotations are not intended to change the run-time behavior of a Java program and because there is not generally a run-time representation of the annotations.
  
  
  
• Annotations on type tests (instanceof) allow the programmer to specify the full type, as in the first justification for annotations on type casts, above. However, the annotation is not tested at run time --- the JVM only checks the base Java type. In the implementation, there is no run-time representation of the annotations on an object's type, so dynamic type test cannot determine whether an annotation is present. This abides by the intention of the Java annotation designers, that annotations should not change the run-time behavior of a Java program.
  
  Annotation of the type test permits the idiom

    if (x instanceof T) {
      ... (T) x ...
    }
  

  to be used with the same annotated type T in both occurrences. By contrast, using different types in the type test and the type cast might be confusing.
  
  To prevent confusion caused by incompatible annotations, an annotation processor could require the annotation parts of the operand and the type to be the same:

    @Readonly Object x;
    if (x instanceof Date) { ... }            // error: incompatible annotations
    if (x instanceof @Readonly Date) { ... }  // OK
    Object y;
    if (y instanceof Date) { ... }            // OK
    if (y instanceof @NonNull Date) { ... }   // error: incompatible annotations
  

  (As with type casts, an annotation processor could implicitly add a missing annotation; this would be more concise but less explicit, and experience will dictate which is better for users.)
  
  As a consequence of the fact that the annotation is not checked at run time, in the following

    if (x instanceof @A1 T) { ... }
    else if (x instanceof @A2 T) { ... }
  

  the second conditional is always dead code. An annotation processor may warn that one or both of the instanceof tests is a compile-time type error.
  
  A non-null qualifier is a special case because it is possible to check at run time whether a given value can have a non-null type. A type-checker for a non-null type system could take advantage of this fact, for instance to perform flow-sensitive type analysis in the presence of a x != null test, but JSR 308 makes no special allowance for it.
  
  
• Annotations on object creation (new) can indicate the type of the newly-created object, which could be statically (at compile time) verified to be compatible with the annotations on the constructor.
  
  
• Annotations on type parameter bounds (extends) and wildcard bounds (extends and super) allow the programmer to fully constrain generic types. Creation of objects with constrained generic types could be statically verified to comply with the annotated bounds.
  
  
• Annotations on class inheritance (extends and implements) are necessary to allow a programmer to fully specify a supertype. It would otherwise be impossible to extend the annotated version of a particular type t (which is often a valid subtype or supertype of t) without using an anonymous class.
  
  These annotations also provide a convenient way to alias otherwise cumbersome types. For instance, a programmer might declare

    final class MyStringMap extends
      @Readonly Map<@NonNull String, @NonEmpty List<@NonNull @Readonly String>> {}
  

  so that MyStringMap may be used in place of the full, unpalatable supertype. (However, also see Section 9.4 for problems with this approach.)
  
  
• Annotations in the throws clauses of method declarations allow programmers to enhance exception types. For instance, programs that use the @Critical annotation from the above examples could be statically checked to ensure that catch blocks for @Critical exceptions are not empty.

3.4  Disambiguating type and declaration annotations

  @NonNegative int balance;
  @GuardedBy("accessLock") long lastAccessedTime;

    @Deprecated
    @NonNull Dimension getSize() { ... }

    @Target({ElementType.METHOD, ...})
    public @interface Deprecated { ... }

    @Target(ElementType.TYPE)
    public @interface NonNull { ... }

3.5  Syntax of array annotations

• within the brackets ([]) of the array syntax: @NonNull Document[@Readonly]
• outside the brackets in prefix notation (before the brackets): @NonNull Document @Readonly []
• outside the brackets in postfix notation (after the brackets): @NonNull Document[] @Readonly
  or, if postfix syntax is adopted for all type annotations: Document @NonNull [] @Readonly

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.

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];
   

  new X[@ReadOnly Y.class.getMethods().length]

  new X[2][@ReadOnly (2) ]

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

4.1  The extended_annotationstructure

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
}

• type_index is an index into the constant pool indicating the annotation type for this annotation.
• num_element_value_pairs is a count of the element_value_pairs that follow.
• Each element_value_pairs table entry represents a single element-value pair in the annotation (in the source code, these are the arguments to the annotation): element_name_index is a constant pool entry for the name of the annotation type element, and value is the corresponding value; for details, see JVMS 3 §4.8.15.1.

4.1.1  The target_type field

• on typecasts, type tests, object creations, local variables, bounds of type parameters of classes and methods, extends and implements clauses of class declarations, and throws clauses of method declarations;
• on a type argument or array type of any of the above;
• on method receivers;
• on a type argument or array type of a field, method, or method parameter.

---

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

Typecasts, type tests, and object creation

    {
        u2 offset;
    } reference_info;

Local Variables

    {
        u2 start_pc;
        u2 length;
        u2 index;
    } reference_info;

Method Receivers

Type Parameter Bounds

    {
        u1 param_index;
        u1 bound_index;
    } reference_info;

    <T extends @A Object & @B Comparable, U extends @C Cloneable>

Class extends and implements Clauses

    {
        u1 type_index;
    } reference_info;

throws Clauses

    {
        u1 type_index;
    } reference_info

Generic Type Arguments or Arrays

    u2 location_length;
    u1 location[location_length];

---

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

5.1  Compiler

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

5.3  Reflection

  @NonEmpty List<@Interned String> foo(@NonNull List<@Opened File> files) @Readonly {...}

5.4  Virtual machine and other tools that manipulate class files

5.5  Other tools

5.6  Java Language Specification

5.7  Java Virtual Machine Specification

6  Testing (TCK, Technology Compatibility Kit)

7  Other annotations

7.1  Duplicate annotations at a location

@Resources({
    @Resource(name = "db1", type = DataSource.class)
    @Resource(name = "db2", type = DataSource.class)
})
public class MyClass { ... }

@Resource(name = "db1", type = DataSource.class)
@Resource(name = "db2", type = DataSource.class)
public class MyClass { ... }

7.2  Annotations on statements

8  Logistical matters

  /*@Readonly*/ Object x;

9  Out-of-scope issues

The last annotations JSR.

9.1  Locations for annotations

Expression annotations.

Implicit Java types in casts.

  (@Language("SQL") String) "select * from foo"

  (@Language("SQL")) "select * from foo"

  @Language("SQL") "select * from foo"

Only certain statements.

9.2  Changes to the annotation type

Subclassing annotations.

Annotations as arguments to annotations

  @DefaultAnnotation(@MyAnnotation)

Positional arguments

9.3  Semantics of annotations

Annotations for specific purposes.

Annotation inheritance.

Default annotations.

  @DefaultAnnotation(NonNull.class, locations={ElementType.LOCAL_VARIABLE})

  @DefaultAnnotation(@MyAnnotation(arg="foo"))

9.4  Type abbreviations and typedefs

  final class MyStringMap extends
    @Readonly Map<@NonNull String, @NonEmpty List<@NonNull @Readonly String>> {}

9.5  Class file syntax

Reducing class file size via use of the constant pool.

10  Related work

Acknowledgments

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 L^AT_EX by H^EV^EA.