Annotations on Java types

JSR 308 working document
Michael D. Ernst
mernst@csail.mit.edu
February 4, 2007

The JSR 308 webpage is https://checkerframework.org/jsr308/. This document is available in PDF at https://checkerframework.org/jsr308/java-annotation-design.pdf.

1  Introduction

We propose an extension to Java's annotation system [Bra04a] that permits annotations to appear on any use of a type, not just on class/method/field/variable declarations, as is the case in Java SE 6. 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 6).

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

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 [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 will serve as a starting point for the JSR 308 expert group, but the expert group has the freedom to explore other approaches or to modify the proposal outlined here.

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). Finally, section 5 describes the modifications to the JDK necessitated by the Java and class file changes.

2  Type qualifiers

One example use of annotation on types is to create custom type qualifiers in the Java language. Type qualifiers are modifiers that provide extra information about a type or variable; they can be thought of as a form of subtyping. 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. 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.

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.

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.

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]. The code in figure 1 demonstrates @NonNull in a sample method. A programmer can annotate any use of a type with the @NonNull annotation. A compiler plug-ins would check that a @NonNull variable is never assigned a possibly-null value, thus enforcing the @NonNull type system.


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


@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-errors.

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

Our system extends Java to allow annotations on any use of a type (whether explicit or implicit, as in the case of method receivers). In Java SE 6, annotations can be written on method parameters and the declarations of classes, methods, fields, and local variables. Our system additionally allows annotations to be written in the following locations, with the given syntax. (The specific annotation names, such as @NonNull, are examples only; this document does not propose any annotations, merely specifying where they can appear in Java code.)

These annotations are necessary in order to fully specify Java classes and methods.

There is no need for new syntax for annotations on return types, because Java already permits an annotation to appear before a method return type. For example, in

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

@Deprecated applies to the method and @NonNull applies to the return type. When an annotation processor encounters an annotation in this position, it can treat the annotation as applying to the method or to the return type, or it can issue a warning/error if the annotation is not sensible in either location. (The annotation processor can choose by using the @Target annotation that appears on the Java definitions of the Deprecated and NonNull interfaces, or in some other way.) This design assumes that there are few anotations that can apply equally well to both methods and return value types, and that have different semantics in the two situations. If such annotations are common, then a different syntax may be warranted.

3.1  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.2  Semantics of array annotations

Consider the following annotated arrays.

    @Readonly Document[] docs1;
    Document[@Readonly] docs2;
    @Readonly Document[][] docs3 = new Document[2][12];
    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.

There are two (incompatible) ways to interpret the syntax, and we must choose one of them. Here, we present both.

Option 1: An annotation before the entire array type binds to the member type that it abuts; @Readonly Document[][] docs4 can be interpreted as (@Readonly Document)[][] docs4. 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]. For example, the declarations above have the following meanings:
docs1 is a mutable one-dimensional array of immutable Documents.
docs2 is an immutable one-dimensional array of mutable Documents.
docs3 is a mutable array, whose elements are mutable one-dimensional arrays of immutable Documents.
docs4 is an immutable array, whose elements are mutable one-dimensional arrays of mutable Documents.
docs5 is a mutable array, whose elements are immutable one-dimensional arrays of mutable Documents.

Option 2: 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]. For example, The declarations above have the following meanings:
docs1 is a inmutable one-dimensional array of mutable Documents.
docs2 is a mutable one-dimensional array of immutable Documents.
docs3 is an immutable array, whose elements are mutable one-dimensional arrays of mutable Documents.
docs4 is a mutable array, whose elements are immutable one-dimensional arrays of mutable Documents.
docs5 is a mutable array, whose elements are mutable one-dimensional arrays of immutable Documents.

4  Class File Format Extensions

Java annotations (including the extended annotations) must be stored in the class file for two reasons. First, they may be part of the interface of a class and, if so, must be available to the compiler (really, to the annotation processor or type-checking plug-in [Dar06]) when compiling clients of the class. Second, since class files may originate from any source, the information may be useful in other contexts, such as compile-time verification.

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.

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 RuntimeVisibleAnnotations attribute is used for annotations that are accessible at runtime using reflection, and the RuntimeInvisibleAnnotations attribute 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: RuntimeVisibleTypeAnnotations and RuntimeInvisibleTypeAnnotations. These attributes are structurally identical to the RuntimeVisibleAnnotations and RuntimeInvisibleAnnotations attributes described above with one exception: rather than an array of annotation elements, RuntimeVisibleTypeAnnotations and RuntimeInvisibleTypeAnnotations contain an array of extended_annotation elements, 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 in the types of a field, the field_info structure (see JVMS 4.6) corresponding to that field stores the Runtime[In]visibleTypeAnnotations attributes. In all other cases, the method_info structure (see JVMS 4.7) that corresponds to the annotations' containing method stores the Runtime[In]visibleTypeAnnotations attributes.

4.1  The extended_annotation Structure

The extended_annotation structure has the following format, which adds target_type and reference_info to the annotation structure defined in JVMS 4.8.16:

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
    {
        ...
    } reference_info;  // new in our proposal
}

The following sections describe the fields of the extended_annotation structure 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 Targettarget_type Value
typecast0x00
typecast generic/array0x01
type test (instanceof)0x02
type test (instanceof) generic/array0x03
object creation (new)0x04
object creation (new) generic/array0x05
method receiver0x06
method receiver generic/array0x07*
local variable0x08
local variable generic/array0x09
method return type0x0A*
method return type generic/array0x0B
method parameter0x0C*
method parameter generic/array0x0D
field0x0E*
field generic/array0x0F
class type parameter bound0x10
class type parameter bound generic/array0x11
method type parameter bound0x12
method type parameter bound generic/array0x13
class extends/implements0x14
class extends/implements generic/array0x15
exception type in throws0x16
exception type in throws generic/array0x17*
Figure 2: Values of target_info 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 delclaration, not the use, of such elements.

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.

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.

One technical challenge is that two differently-annotated expressions might be combined via common subexpression elimination.

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 JVMS 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 (i.e., 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>>

 

Annotationlocation_lengthlocation
@Anot applicable
@B10
@C20, 0
@D30, 0, 0
@E30, 0, 1
@F30, 0, 2
@G11
@H21, 0
Figure 3: Values of the location_length and location fields for a sample declaration.

5  Required Tool Modifications

The implementation of extended annotations builds on the existing framework for Java annotations.

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.

When generating code, the compiler must emit the attributes described in section 4.

Similar modifications need to be made to other compilers, IDEs, and related tools, such as Eclipse, IDEA, and ASM (https://asm.ow2.io).

The java.lang.reflect.* APIs give access to annotations on classes, the signatures of methods, 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). We do not plan to provide access to annotations on casts, type parameter names, or other 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.

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 typecasts, receivers, type arguments, and local variables. 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.

No modifications to the virtual machine are necessary.

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 Index File Specification” (https://checkerframework.org/jsr308/index-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 or are building a variety of 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.

6  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.

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.

Annotations on blocks or loops, which are not currently permitted by Java, could be useful for properties such as atomicity/concurrency. Such an extension would require defining both Java syntax and convention for storing the information in the class file.

7  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 reference implementation is built on javac, but once javac is open-sourced, we will be able to share the reference implementation more widely.

To ease the transition from standard Java SE 6 code to code with the extended annotations, the reference 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.

Acknowledgments

We thank the members of the JSR 308 mailing list for their comments and suggestions. We welcome additional feedback.

References

[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.
[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.
[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.
[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.
[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.
[EC06]
Michael D. Ernst and Danny Coward. JSR 308: Annotations on Java types. https://jcp.org/en/jsr/detail?id=308, October 17, 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.
[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.
[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.
[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.
[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.
[PØ95]
Jens Palsberg and Peter Ørbæk. Trust in the λ-calculus. In SAS95, 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 3rd Workshop on Formal Techniques for Java Programs, Budapest, Hungary, June 18, 2001. Revised.
[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.

This document was translated from LATEX by HEVEA.