SRC Technical Note

2000-002

October 12, 2000

ESC/Java User's Manual

K. Rustan M. Leino, Greg Nelson, and James B. Saxe

Compaq
Compaq Computer Corporation
Systems Research Center
130 Lytton Avenue
Palo Alto, CA 94301
http://research.compaq.com/SRC/

Copyright © 1999, 2000 Compaq Computer Corporation. All rights reserved

Limitation of liability:  This publication and the software it describes are provided ``as is'' without warranty of any kind, express or implied, including, but not limited to, the implied warranties of merchantability, fitness for a particular purpose, or non-infringement.

This publication could include technical inaccuracies or typographical errors.  Furthermore, the Compaq Extended Static Checker for Java (ESC/Java) is currently under development.  Compaq therefore expects that changes will occur in the ESC/Java software and documentation, from time to time.  Compaq reserves the right to adopt such changes, or to cause or recommend that ESC/Java users adopt such changes, upon such notice as is practicable under the circumstances or without any notice, in its discretion.

The Compaq Extended Static Checker for Java (ESC/Java) is not a product of Sun Microsystems, Inc.

Compaq is a registered trademark of Compaq Computer Corporation.  Java is a trademark or registered trademark of Sun Microsystems, Inc.  UNIX is a registered trademark in the United States and other countries, exclusively licensed through X/Open Company, Ltd.  Windows is a registered trademark of Microsoft Corporation.  PostScript is a registered trademark of Adobe Systems, Inc.  All other trademarks or registered trademarks mentioned herein are the property of their respective holders.

Abstract

The Compaq Extended Static Checker for Java (ESC/Java) is a programming tool that attempts to find common run-time errors in Java programs by static analysis of the program text.  Users can control the amount and kinds of checking that ESC/Java performs by annotating their programs with specially formatted comments called  pragmas.  This manual is designed to serve both as an introduction to ESC/Java and as a reference manual. It starts by providing an overview of ESC/Java through an illustrative example of its use and a summary of its features, and then goes on to document all the pragmas supported by ESC/Java and all the kinds of warnings that it generates.  Appendices provide a brief sketch of ESC/Java's implementation, information about obtaining ESC/Java, and some discussion of its limitations.

Preface

The Compaq Extended Static Checker for Java (ESC/Java) is a programming tool that attempts to find common run-time errors in Java programs by static analysis of the program text.  Users can control the amount and kinds of checking that ESC/Java performs by annotating their program with specially formatted comments called  pragmas.  This manual starts by providing an overview of ESC/Java through an illustrative example of its use and a summary of its features, and then goes on to document all the pragmas supported by ESC/Java and all the kinds of warnings that it generates.  It also provides basic information about running ESC/Java.

This manual documents Version 1.2.2 of ESC/Java, built on October 12, 2000.  We sometimes speak of ``the current ESC/Java'--rather than just ``ESC/Java''--to emphasize that particular features, bugs, or limitations under discussion are artifacts of the Version 1.2.2 implementation and may be subject to change in future versions.  Of course there is no guarantee that all such aspects of ESC/Java will in fact change (nor that other aspects will remain unchanged) as the tool evolves.

This manual is designed to serve both as an introduction to ESC/Java and as a reference manual.  First-time readers may prefer to skip the portions marked ``Fine point(s)'' as well as some other parts that we have indicated.  On the other hand, the extended example in section 0 should be particularly helpful to first-time readers.

For a much abridged treatment of the information in this manual, see the ``ESC/Java Quick Reference'' [SLS00].  The Quick Reference lists most of the specification language features described in sections 2 and 3 of this manual and all the warning types described in section 4, giving very brief descriptions of each.  While it necessarily omits numerous examples, tips, motivating discussions, and technical details found in the present manual, it will still be of interest both the new reader seeking a whirlwind tour of ESC/Java's features and to the experienced user seeking a quick reminder about some ESC/Java feature.

Although ESC/Java contains a full Java program verifier, the goal of ESC/Java is not to provide formally rigorous program verification.  Rather, it is to help programmers find some kinds of errors more quickly than they might be found by other methods, such as testing or code reviews.  Consequently, ESC/Java embodies engineering trade-offs among a number of factors including the frequency of missed errors, the frequency of false alarms, the amount of time used by the tool, the effort required to learn and use the annotation language, and the effort required to implement the tool.  In this manual we attempt to give a precise description of the syntax, type-checking, and other linguistic rules of the annotation language, as well as a clear though informal description of the meanings of the various pragmas.  While we discuss potential sources of missed errors or false alarms at various places in the manual, including a summary in appendix C, we do not attempt to characterize precisely the degree of (in)accuracy of ESC/Java's checking

In many places we cite sections of The Java Specification Language, by James Gosling, Bill Joy, and Guy Steele [JLS].  For example, the notation ``[JLS, 19.2]'' refers to section 19.2 of The Java Language Specification.  The list of references at the end of this manual gives bibliographic information for this and other works cited herein.

A specification notation and set of tools related to ESC/Java is the Java Modeling Language (JML) [LBR99, LBR00, LLPRJ00].  Through a collaborative effort, we have attempted to make the JML specification language and the ESC/Java annotation language as similar as practical, with JML providing a superset of the features of ESC/Java.  The goals of the two languages are different, so differences in the notations remain.  However, many programs annotated with ESC/Java annotations should be amenable to processing with other JML tools, and programmers who learn one language should have little trouble picking up the other as well.

Acknowledgments

ESC/Java was originally designed and implemented at the Compaq Systems Research Center (SRC) by Cormac Flanagan, Mark Lillibridge, Raymie Stata, and the authors.  Todd Millstein implemented ESC/Java's execution trace facility and helped with other aspects of ESC/Java.  Caroline Tice and Rajeev Joshi lent helping hands with miscellaneous aspects of the implementation, including reducing ESC/Java's memory footprint (Tice) and getting the build recipe for the Simplify theorem prover to work on multiple platforms (Joshi).

The ESC/Java project is a follow-on to an earlier extended static checking project at SRC targeting the Modula-3 language [DLNS98], and continues to use the Simplify theorem prover developed as part of that project.

The authors thank our colleagues who have offered comments on earlier versions of this manual. Allan Heydon, David Jefferson, Mark Lillibridge, Silvija Seres, and Caroline Tice have been particularly helpful in this regard.  Silvija Seres compiled the initial version of the ESC/Java Quick Reference [SLS00] from an earlier version of this manual.  We and the other implementers of ESC/Java have benefited from the feedback of early users, including Sanjay Ghemawat, Steve Glassman, Allan Heydon, David Jefferson, Marc Najork, Keith Randall, and Silvija Seres.  Gary Leavens played a major role in our attempt to remove gratuitous incompatibilities between ESC/Java and JML, and helped us to improve the ESC/Java annotation language in the process.

Contents

Preface

Acknowledgments

Contents

0  An illustrative example of using ESC/Java

0.0  Scene 0:  We write a class declaration.
0.1  Scene 1:  We run ESC/Java, and it warns of two potential null dereferences.
0.2  Scene 2:  We write a requires (precondition) pragma for the Bag  constructor.
0.3  Scene 3:  We add a non_null pragma for the field a.
0.4  Scene 4:  We correct a bug in Bag.extractMin.
0.5  Scene 5:  We take no action for a redundant warning.
0.6  Scene 6:  We supply a precondition for Bag.extractMin.
0.7  Scene 7:  We run ESC/Java again and it still issues a warning.
0.8  Scene 8:  We supply an invariant pragma relating n to a.lenght. [sic]
0.9  Scene 9:  ESC/Java notices a typographical error.
0.10  Scene 10:  Our efforts come to a happy conclusion.
1  An overview of ESC/Java and of this manual 2  ESC/Java pragmas
2.0  Rules about where pragmas may occur
2.0.0  ESC/Java pragmas must occur within pragma-containing comments.
2.0.1  There are four syntactic categories of pragmas.
2.0.2  ESC/Java sometimes allows pragmas to contain nested pragmas or comments.
2.1  The most basic pragmas
2.1.0  nowarn pragma
2.1.1  assert pragma
2.1.2  assume pragma
2.1.3  unreachable pragma
2.2  Some remarks concerning assert and assume
2.2.0  The assume pragma should be used with judgment.
2.2.1 Most ESC/Java pragmas are just fancy forms of assert and assume.
2.2.2  A nowarn pragma suppresses warnings by turning assertions into assumptions.
2.2.3  A helpful tip:  Experiments with assert and assume pragmas can help you understand ESC/Java's behavior and debug your annotated code.
2.3  Pragmas for specifying routines
2.3.0  requires pragma
2.3.1  modifies pragma
2.3.1.0  target fields
2.3.2  ensures pragma
2.3.3  A note on the interaction of modifies and \old
2.3.4  exsures pragma
2.3.5  also_ensures pragma
2.3.6  also_exsures pragma
2.3.7  also_requires pragma
2.3.8  also_modifies pragma
2.4  Pragmas for specifying data invariants
2.4.0  non_null pragma
2.4.1  invariant pragma
2.4.2  axiom pragma
2.4.3  loop_invariant pragma
2.5  Pragmas affecting conditions under which variables may be referenced
2.5.0  spec_public pragma
2.5.1  readable_if pragma
2.5.2  uninitialized pragma
2.6  Pragmas concerning ghost variables
2.6.0  ghost pragma
2.6.1  set pragma
2.6.2  Examples using ghost variables
2.7  Pragmas for specifying synchronization
2.7.0  monitored_by pragma
2.7.1  monitored pragma
2.7.2  Examples illustrating race and deadlock checking
3  Specification expressions
3.0  Specification types
3.1  Restrictions
3.2  Additions
3.2.0  \type
3.2.1  \typeof
3.2.2  \elemtype
3.2.3  Subtype:  <:
3.2.4  Examples involving \TYPE, \type, \typeof, \elemtype, and <:
3.2.5  \lockset
3.2.6  Membership in lock sets:  [ ]
3.2.7  Lock order: < and <=
3.2.8  \max
3.2.9  Implication: ==>
3.2.10  \forall
3.2.11  \exists
3.2.12  \nonnullelements
3.2.13  \fresh
3.2.14  \result
3.2.15  \old
3.2.16  \lblneg and \lblpos
3.2.17 owner
3.3 Scoping, name resolution, and access control in specification expressions
4  Warnings
4.0  Parts of ESC/Java warning messages
4.1  ArrayStore warning
4.2  Assert warning
4.3  Cast warning
4.4  Deadlock warning
4.5  Exception warning
4.6  IndexNegative warning
4.7  IndexTooBig warning
4.8  Invariant warning
4.9  LoopInv warning
4.10  NegSize warning
4.11  NonNull warning
4.12  NonNullInit warning
4.13  Null warning
4.14  OwnerNull warning
4.15  Post warning
4.16  Pre warning
4.17  Race warning
4.18  Reachable warning
4.19  Unreadable warning
4.20  Uninit warning
4.21  ZeroDiv warning
5  Command-line options and environment variables
5.0  -suggest
5.1  Specification (.spec) files and the ESC/Java's class path
5.1.0  File reading modes
5.1.1  The ESC/Java class path (-classpath, CLASSPATH, -bootclasspath)
5.1.2  Specification (.spec) files
5.1.3  How ESC/Java decides which files to read and in which modes
5.1.4  -depend
6  Java language support and limitations

Appendix A:  Overview of how ESC/Java works

Appendix B:  Installing and using ESC/Java at your site

Appendix C:  Sources of unsoundness and incompleteness ESC/Java

C.0  Known sources of unsoundness
C.0.0  Trusting pragmas
C.0.1  Loops
C.0.2  Object invariants
C.0.3  Modification targets
C.0.4  The also_modifies and also_requires pragmas
C.0.5  Multiple inheritance
C.0.6  Arithmetic overflow
C.0.7  Ignored exceptional conditions
C.0.8  Constructor leaking
C.0.9  Static initialization
C.0.10  Class paths and .spec files
C.0.11  Shared variables
C.0.12  Initialization of fields declared non_null
C.0.13  String literals
C.0.14  Search limits in Simplify
C.0.15  Integer arithmetic bug in Simplify
C.1  Some sources of incompleteness
C.1.0  Incompleteness of the theorem-prover
C.1.1  Incomplete modeling of Java semantics
C.1.2  Modular checking
References

0  An illustrative example of using ESC/Java

To give the reader a general idea of what ESC/Java does and how to use it, we begin with an example illustrating some salient features of ESC/Java through its application to a simple class declaration deliberately seeded with some errors.

0.0  Scene 0:  We write a class declaration.

Our example is the class Bag declared in a file Bag.java as follows:
line
 1:  class Bag {
 2:    int[] a;
 3:    int n;
 4:
 5:    Bag(int[] input) {
 6:      n = input.length;
 7:      a = new int[n];
 8:      System.arraycopy(input, 0, a, 0, n);
 9:    }
10:
11:    int extractMin() {
12:      int m = Integer.MAX_VALUE;
13:      int mindex = 0;
14:      for (int i = 1; i <= n; i++) {
15:        if (a[i] < m) {
16:          mindex = i;
17:          m = a[i];
18:        }
19:      }
20:      n--;
21:      a[mindex] = a[n];
22:      return m;
23:    }
24:  }
A copy of this program is in escjavaRoot/examples/0.0/Bag.java, where escjavaRoot denotes the (site-specific) top-level directory for ESC/Java (see appendix B).  The idea is that an object x of class Bag represents a multiset (also known as a ``bag'') of integers in the form of integer array x.a together with an integer x.n, where the elements of the multiset are the first x.n elements of the array.  In our example declaration, we define a constructor that creates a Bag from an array, and a single method extractMin that finds, removes, and returns the minimal element of a Bag. The extractMin method iterates over the first this.n elements of this.a, keeping track of the smallest one in the local variable m .  After finding the smallest element of this.a,  it copies the element at the highest used position of x.a into the position formerly occupied by the minimum element, decreases the count of used elements, and returns the value that was saved in m .

0.1  Scene 1:  We run ESC/Java, and it warns of two potential null dereferences.

To compile Bag.java, we would type the command line:
javac Bag.java
To check our definition of class Bag with ESC/Java, we instead type the following similar command line:
escjava Bag.java
ESC/Java then produces the following output:
Bag.java:6: Warning: Possible null dereference (Null)
    n = input.length;
             ^
Bag.java:15: Warning: Possible null dereference (Null)
      if (a[i] < m) {
           ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:15: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:21: Warning: Possible null dereference (Null)
    a[mindex] = a[n];
                 ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

Bag.java:21: Warning: Possible negative array index (IndexNegative)
    a[mindex] = a[n];
                 ^
Execution trace information:
    Completed 0 loop iterations in "Bag.java", line 14, col 4.

5 warnings

Remark:  Actually,  the above is the output generated by the command

escjava -quiet Bag.java
The normal output of ESC/Java also includes various progress messages and timing information which are omitted here.

Remark:  Some of the messages above include a part marked as ``Execution trace information''.  We say more about execution traces below, particularly in section 4.0, but will not discuss them further in the course of this introductory example.

0.2  Scene 2:  We write a requires (precondition) pragma for the Bag constructor.

ESC/Java's first warning is that the attempt on line 6 to access input.length might fail because input might be null.  We now must decide what to do about this warning.

One approach would be to decide that the implementation of the constructor is incorrect.  Following this approach, we would modify the constructor to test for a null argument and, for example, construct an empty multiset:

  Bag(int[] input) {
    if (input == null) {
      n = 0;
      a = new int[0];
    } else {
      n = input.length;
      a = new int[n];
      System.arraycopy(input, 0, a, 0, n);
    }
  }
This would indeed eliminate the first warning.  Instead, however, we will continue our example by illustrating a second approach, in which we decide that the implementation of the constructor is correct, but that we do not intend for the constructor ever to be called with a null argument.  We inform ESC/Java of this decision by adding an annotation to the constructor declaration:
       //@ requires input != null;
       Bag(int[] input) {
         n = input.length;
       ...
When the character @ is the first character after the initial // or /* of a Java comment, as in the first line of the program fragment above, ESC/Java expects the body of the comment to consist of a sequence of ESC/Java annotations, known as pragmas.  The requires pragma above specifies a precondition for the constructor, that is, a boolean expression which must be true at the start of any call.  When checking the body of a method or constructor that is annotated with a precondition, ESC/Java can assume the truth of the precondition to confirm the absence of errors in the body (for example, the absence of a null dereference during the evaluation of input.length in the code fragment above).  When checking code that calls a method or constructor annotated with a precondition, ESC/Java will issue a warning if it cannot confirm that the precondition (with the values of the actual parameters substituted for the formal parameter names) would always evaluate to true at the call site.

0.3  Scene 3:  We add a non_null pragma for the field a.

So much for the first warning.  We now turn our attention to the second warning:
Bag.java:15: Warning: Possible null dereference (Null)
      if (a[i] < m) {
           ^
Here, ESC/Java is warning that the array variable a (actually this.a) might be null.  We could deal with this warning by either of the approaches discussed above in connection with the first warning--that is, by adding the precondition requires a != null to the extractMin method, or by adding special code for the case a == null. However ESC/Java offers yet another choice, which is to specify that the a field of any Bag is always supposed to be non-null.  To do this, we annotate the declaration of a with a non_null pragma:
     class Bag {
       /*@ non_null */ int[] a;
       ...
This causes ESC/Java to assume that the a field of any Bag object is itself non-null (and thus can safely be dereferenced).  Conversely, it causes ESC/Java to issue a warning for any assignment to the a field of a Bag, if it cannot confirm that the expression being assigned will have a non-null value at run time.  Furthermore ESC/Java will check that every Bag constructor initializes the a field of the constructed object to a non-null value.

0.4  Scene 4:  We correct a bug in Bag.extractMin.

We now consider the third warning:
Bag.java:15: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^
Examining the program, we now find a genuine bug.  The for loop starting on line 15 (in the original program) examines array elements a[1] through a[n], but array indexing in Java is zero based.  We correct the line to read
        for (int i = 0; i < n; i++) {

0.5  Scene 5:  We take no action for a redundant warning.

The fourth warning
Bag.java:21: Warning: Possible null dereference (Null)
    a[mindex] = a[n];
                 ^
requires no action, as the non_null pragma we added in section 0.3 already prevents a from being null.  In other words, the second and fourth warnings complain about the same problem.
Remark:  ESC/Java often avoids issuing such redundant warnings.  Note, for example, that it doesn't complain about the expression a[m] on (original) line 17, or the expression a[mindex] on the left hand side of the assignment on (original) line 21.  However, it does not avoid them in all cases.  A detailed description of the circumstances in which ESC/Java will or will not issue multiple warnings with the same underlying cause is beyond the scope of this manual.

0.6  Scene 6:  We supply a precondition for Bag.extractMin.

We now consider the last of the five warnings:
Bag.java:21: Warning: Possible negative array index (IndexNegative)
    a[mindex] = a[n];
                 ^
The problem is that the code in (original) lines 20-21 removes an element from the bag even when the bag is already empty (that is, when this.n == 0 on entry to extractMin).  ESC/Java has called our attention to the need for another design decision:  do we add special code to handle the situation when extractMin is called on an empty bag, or do we add a precondition forbidding such calls?  Let's try the latter course:
12:    //@ requires n >= 1;
13:    int extractMin() {

0.7 Scene 7:  We run ESC/Java again and it still issues a warning.

With all the changes described above, our example program now reads:
 1:  class Bag {
 2:    /*@ non_null */ int[] a;
 3:    int n;
 4:
 5:    //@ requires input != null;
 6:    Bag(int[] input) {
 7:      n = input.length;
 8:      a = new int[n];
 9:      System.arraycopy(input, 0, a, 0, n);
10     }
11:
12:    //@ requires n >= 1;
12:    int extractMin() {
13:      int m = Integer.MAX_VALUE;
14:      int mindex = 0;
15:      for (int i = 0; i < n; i++) {
16:        if (a[i] < m) {
17:          mindex = i;
18:          m = a[i];
19:        }
20:      }
21:      n--;
22:      a[mindex] = a[n];
23:      return m;
24:    }
25:  }
We now run ESC/Java again and it produces the following warning:
Bag.java:17: Warning: Array index possibly too large (IndexTooBig)
      if (a[i] < m) {
           ^

0.8  Scene 8:  We supply an invariant pragma relating n to a.length.

It may appear that ESC/Java is still complaining about the bug we thought we'd fixed in section 0.4, but further study reveals a different problem:  ESC/Java has no reason to expect that n, which we intend to be the length of the meaningful prefix of a, will in fact be at most a.length.   We can express this intention with an invariant pragma:
 1:  class Bag {
 2:    /*@ non_null */ int[] a;
 3:    int n;
 4:    //@ invariant 0 <= n & n <= a.lenght;
...
Roughly speaking, ESC/Java treats an invariant as an implicit postcondition of every constructor and as both a precondition and postcondition of every method.  The semantics of invariant pragmas--and all other ESC/Java pragmas--are described in greater detail in section 2 below.  The full rules about expressions that can occur in pragmas (called specification expressions) are given in section 3.  For now, we remark that since specification expressions are not actually executed, the unconditional logical operators & and | are interchangeable (except for binding power) in specification expressions with the respective conditional operators && and ||.

0.9  Scene 9:  ESC/Java notices a typographical error.

When we run ESC/Java again, the result is:
Bag.java:4: Error: No such field in type int[]
  //@ invariant 0 <= n & n <= a.lenght;
                                ^
Caution: Turning off extended static checking due to type error(s)
1 caution
1 error

0.10  Scene 10:  Our efforts come to a happy conclusion.

Whoops!  Our invariant pragma had a spelling error. We correct it to read
 4:    //@ invariant 0 <= n & n <= a.length;
and try again.  This time ESC/Java runs without reporting any further complaints.

The file escjavaRoot/examples/0.10/Bag.java contains a copy of the final version of the Bag class.

1  An overview of ESC/Java and of this manual

In this section we summarize the principal features of ESC/Java. While some of the things we say here reiterate points made in our example of section 0, we also describe a number of features of ESC/Java that are not discussed at all in section 0.  Moreover, we address a number of points that were glossed over in section 0, and that possibly raised questions in the mind of the perceptive reader.  Throughout this section we refer the reader to later parts of this manual where various topics are discussed in more detail.

2  ESC/Java pragmas

In this section we describe all the kinds of ESC/Java pragmas, the places where they can occur, and (informally) what they mean.  We begin by giving some general information about where pragmas can occur, and then go on to describe the individual pragmas.

Many pragmas can contain expressions--called specification expressions--which are similar to Java expressions, but with a few constructs legal in Java expressions being forbidden and a number of added constructs being permitted.  We mention some of the added constructs in connection with pragmas where they are of use, but defer a detailed description of specification expressions to section 3.

Most pragmas are ways of asking ESC/Java to produce warnings if certain user expectations about the behavior of the annotated program may be wrong.  We will often say that ESC/Java ``checks'' that some condition x holds at a particular control point when it would be more precise to say that ESC/Java issues a warning message if it cannot prove that x holds at that point.  Keep in mind that in addition to the possibility that x might fail, the warning may also be issued because the annotations are inadequate to imply that x holds, because the theorem-prover's deductive power is inadequate to complete the proof, or because ESC/Java's model of Java semantics is incomplete.

2.0  Rules about where pragmas may occur

2.0.0 ESC/Java pragmas must occur within pragma-containing comments.

ESC/Java looks for pragmas within certain specially formatted comments.  Specifically: Many pragmas end with an optional semi-colon ( ;opt ).  If such a pragma is followed by another pragma in the same pragma-containing comment, then this semi-colon is required.

2.0.1  There are four syntactic categories of pragmas.

Pragmas are divided into four syntactic categories according to the places in a program where they can sensibly be used.  All pragmas in any single pragma-containing comment must be of the same syntactic category. Fine points

A modifier pragma that modifies a routine (method or constructor) declaration may appear either in any of the following places:

The semantics of a routine modifier pragma is independent of whether the pragma appears lexically before or after the signature of the routine.  Routine modifier pragmas are described further in section 2.3.

A modifier pragma that modifies a variable declaration may appear either in the usual place for modifiers near the beginning of the declaration or just before the final semicolon.  The pragma applies to all variables declared in the declaration, and its semantics is independent of its position within the declaration.  For convenient reference, here is a table listing ESC/Java pragmas that can modify variable declarations, the sections of this manual where they are described, and the kinds of declarations they are allowed to modify:

Note that ESC/Java sometimes allows modifier pragmas in declarations of local variables (including those declared in the ForInit of a for statement [JLS, 14.12]) and formal parameters.

Particular pragmas may have further restrictions on where they may occur beyond those given above.  These restrictions are described in the sections describing the respective pragmas.

2.0.2  ESC/Java sometimes allows pragmas to contain nested pragmas or comments.

Situations sometimes arise where it is convenient to nest a comment inside a pragma, or where it is convenient--or even necessary--to nest a pragma inside another pragma.  In particular, this is the only way to annotate a ghost field (see section 2.6.0) with a modifier pragma.  We describe here the rules governing such nesting.  [Readers may wish to skip the remainder of this section on first reading of the manual, or until occasion for using such nesting presents itself.]

In the current ESC/Java, a pragma-containing comment (call it inner) may be nested inside pragma-containing comment (outer) only in the following cases:

(1)  each pragma in inner is a lexical (nowarn) pragma (see section 2.1,0), or

(2)  each pragma in inner is a modifier pragma for a ghost variable declared in outer (see section 2.6.0 for further details).

Furthermore, outer must not itself be nested inside another pragma-containing comment. (However, outer may be of the form <esc>...</esc>, which must of necessity occur inside a Java documentation comment).

Any pragma-containing comment outer--even a nested one--may have an ordinary (i.e., non-pragma-containing) comment inner nested inside it.

Also, there are some restrictions concerning the syntactic forms of a nested (ordinary or pragma-containing) comment inner and the enclosing pragma-containing comment outer, as given in the following table and the associated notes.  These restrictions ensure that the portions of the input file that ESC/Java regards as comments or pragmas will be precisely those regarded as comments by Java compilers.  Each row of the table corresponds to a syntactic form of outer and each column corresponds to a syntactic form of inner.  Entries tell whether each specific form of nesting is allowed and reference notes giving any additional restrictions on allowed forms of nesting and explanations of why forbidden forms of nesting are forbidden.

inner   //...   //@...   /*...*/   /*@...*/   /**...*/ 
outer
 
//@...inner... ok(1) ok(1) ok(2) ok(2) no(3)
/*@...inner...*/ ok(4) ok(4) no(5) no(5) no(5)
<esc>...inner...</esc> ok(6) ok(6) no(5) no(5) no(5)
Notes:
(1)  ESC/Java considers inner to extend to the end of the line on which it begins.
(2)  inner must be entirely on one line (because Java defines outer to end at the end of the line).
(3)  The current ESC/Java might accept this form of nesting, but it is strongly deprecated.  There is no good reason to use it, and javadoc(5) will not recognize inner as a documentation comment.
(4)  ESC/Java considers inner to extend either to the end of the line or up to the closing */ of outer, whichever is earlier.
(5)  These forms of nesting are forbidden because Java does not allow comments of the form /*...*/ to be nested inside each other.  Thus Java compilers would interpret the closing */ of inner as ending outer.
(6)   ESC/Java considers inner to extend either to the end of the line or up to the closing </esc> of outer, whichever is earlier.
Examples

Here are some examples of legal nesting of comments and pragmas inside pragmas:

Here are some examples of illegal nesting:
Tip:  ESC/Java's warning messages for these two examples of illegal nesting fail to give the line number on which the error occurs (but do indicate that the problem is an "unterminated comment").  You can localize the error by running a Java compiler on your program (which is generally a good thing to do before running ESC/Java, anyway).

2.1  The most basic pragmas

In this section we describe the simplest ESC/Java pragmas: nowarn, assume, assert, and unreachable.  The nowarn pragma is essentially a blunt instrument for getting ESC/Java to shut up about uninteresting warnings, thus helping to prevent ESC/Java's known imperfections and limitations from becoming major sources of user annoyance.  The assert and assume pragmas are the fundamental pragmas of which most others are simply more elaborate forms (see section 2.2.1).  They may also be useful in their own right (see particularly section 2.2.3).

2.1.0  nowarn pragma

A nowarn pragma is a lexical pragma.  It has the form:
nowarn L ;opt
where L is a (possibly empty) comma-separated list of warning types from the following list:
ArrayStore      Invariant       Post
Assert          LoopInv         Pre
Cast            NegSize         Race
Deadlock        NonNull         Reachable
Exception       NonNullInit     Unreadable
IndexNegative   Null            Uninit
IndexTooBig     OwnerNull       ZeroDiv
The pragma suppresses any warning messages of the types in L that are associated with the line on which the pragma appears.  If L is empty, all warning types are suppressed.   See section 4 for descriptions of the different types of warnings.

Fine points

Some ESC/Java warning messages refer to two source code locations, namely (1) a location indicating the control point where an error could potentially occur at run-time, and (2) the location of a pragma (or, occasionally, a Java declaration) associated with the warning.  In such cases the warning can be suppressed by a nowarn pragma on either of the indicated source lines.

The nowarn pragma is potentially unsound, and should be used only in cases where the programmer is willing to take responsibility that the suppressed warnings are really false alarms.  The primary intended use of nowarn pragmas is where the suppressed warnings concern situations that are impossible in practice, but for reasons beyond ESC/Java's ability to discover.  Another use would be to suppress warnings for circumstances that are actually harmless (and where the programmer is willing to take responsibility that they are harmless).  For example, a nowarn pragma might be used to suppress a warning for a null dereference if the resulting exception would be caught by a handler (but in such a case the current ESC/Java will not check that there actually is a handler, nor will it check for any errors that might occur during or after execution of the handler).

The nowarn pragma suppresses warnings on a line-by-line basis.  ESC/Java also provide command-line options that enable and disable checking at a much coarser grain (see the descriptions of the -nowarn, -warn, -start, -routine, and -routineIndirect options on the escjava(1) man page).

Unlike warning messages, ESC/Java error messages cannot be suppressed by nowarn pragmas.  Error messages report conditions that prevent ESC/Java from making enough sense of the program to do further checking.

Bug:  The current ESC/Java does not allow another pragma to follow a nowarn pragma in the same pragma-containing comment.  Since the only lexical pragma in the current ESC/Java is nowarn, and since you can say with one nowarn pragma anything that you can say with two, this should not cause problems in practice.

2.1.1  assert pragma

An assert pragma is a statement pragma.  It has the form
assert E ;opt
where E is boolean specification expression.  The pragma causes ESC/Java to issue a warning if it cannot establish that E is true whenever control reaches the pragma.
 

2.1.2  assume pragma

An assume pragma is a statement pragma.  It has the form
assume E ;opt
where E is boolean specification expression.  The pragma causes ESC/Java to assume that E is true whenever control reaches the pragma.  In other words, for any execution path in which E is false when control reaches the pragma, ESC/Java ignores the path from that point on.

Example

The usual purpose of an assume pragma is to supply ESC/Java with some piece of information that is incapable of deducing on its own, thereby preventing ESC/Java from generating spurious warnings.  In the code fragment

22:        // start complicated computation guaranteed to leave i != 0
...       ...
146:       // end of complicated computation
147:       //@ assume i != 0;
148:       if (b) {
149:         g = h/i;
150:       } else {
151:         h = g/i + g/j;
152:       }
the assume pragma at line 147 prevents ESC/Java from warning that the division by i in lines 149 and 151 may give rise to an ArithmeticException, but ESC/Java will still generate a warning about the division by j in line 151 unless it can deduce that j will never be zero when control reaches that point.

Fine points

Like the nowarn pragma, the assume pragma is potentially unsound, and should be used only if the programmer is willing to take responsibility that E holds whenever control reaches the pragma (or at least is willing to give up further checking for any execution paths on which E is false).  When faced with the choice of using either an assume pragma or a nowarn pragma to suppress a spurious warning, it is preferable to use an assume pragma (if it is practical to do so), since the assume pragma more explicitly documents your assumptions about the behavior of the program.

The sentence ``In other words, for any execution path ... from that point on.'' may have seemed unclear to some readers.  For some more examples of its meaning, consider the following code fragment:

31:      if (u != null | v != null) e = 10;
32:      if (v == null) {
33:        w = a.f;
34:        //@ assert b != null;
35:        //@ assume a != null & b != null & c != null & d != null & e > 0;
36:        x = c.f;
37:        //@ assert d != null;
38:      } else {
39:        c = new ...;
40:        d = v;
41:      }
42:      y = a.g;
43:      //@ assert b != null;
44:      z = c.g;
45:      //@ assert d != null;
46:      //@ assert e > 0;
When ESC/Java checks this code:
  • ESC/Java will not warn of a possible dereference of null at line 36 or of a possible assertion failure at line 37, because the only way control can reach those lines is by first reaching the assume pragma at line 35.
  • The assume pragma at line 35 will not prevent ESC/Java from issuing warnings about line 33  and/or 34, because control can reach those lines before reaching line 35.
  • ESC/Java might issue warnings about line 42 and/or 43, because control might reach those lines by some path that does not first reach line 35.  This can happen if control can reach line 32 with a or b being null and x being non-null.
  • ESC/Java will not warn of a possible dereference of null at line 44 or of a possible assertion failure at line 45 or 46.  Every execution path that reaches line 44 first either reaches line 35 (in which case ESC/Java considers further execution of that path only for cases where the expression in the assume pragma would evaluate to true) or reaches lines 39 and 40 (in which case the c and d are assigned non-null values, and e must already have been assigned a nonnegative value at line 31).
    • For a concise formal description of the semantics of assume, see [LSS99].

    2.1.3  unreachable pragma

    An unreachable pragma is a statement pragma.  It has the form
    unreachable ;opt
    The pragma is semantically equivalent to
    assert false;
    except for giving rise to a different warning message.

    2.2  Some remarks concerning assert and assume

    [Readers anxious to ``cut to the chase'' may skip this section on first reading.  Others, however, may find that this material aids their intuition about how ESC/Java works.]

    The assert and assume pragmas introduced in section 2.1 are in some sense the most basic ESC/Java pragmas.  We make some remarks about them here before going on to describe the rest.

    2.2.0  The assume pragma should be used with judgment.

    An assume pragma resembles an assert pragma in that each states a condition that the programmer believes to hold whenever control reaches a certain point in the program.  The difference is that ESC/Java checks--that is, issues a warning if it cannot establish--the condition (called an asserted condition or assertion) in an assert pragma, but ESC/Java takes the assumed condition (or assumption) in an assume pragma for granted.  That is, the programmer takes responsibility that assumed conditions will hold.

    Put another way, the assume pragma allows the programmer to trade spurious warnings (incompleteness) for possible missed warnings (unsoundness).  Thus, you should use assume pragmas with care, lest by supplying an incorrect assumption you suppress warnings of genuine errors.  For example, ESC/Java will not warn of any error that might occur downstream in the execution path from the line:

        x = null; //@ assume x != null;
    since there can be no execution path where the assumption holds after the assignment is performed.

    On the other hand, there will be cases where assume pragmas (or nowarn pragmas, which call for similar caution in their use) will be the only practical means to eliminate spurious warnings.  Also, while it is sometimes possible to eliminate spurious warnings by means that don't carry the same risks of missed warnings, some judgment must be exercised as to whether the improved assurance of correctness will be worth the increased effort in any particular case.

    2.2.1  Most ESC/Java pragmas are just fancy forms of assert and assume.

    The ESC/Java annotation language includes over twenty different kinds of pragmas, but to a first approximation they are mainly more or less elaborate ways of adding assertions (i.e., claims about the program state that are checked by the ESC/Java) and/or assumptions (i.e., claims that are taken for granted by ESC/Java) at different points in the program.  Indeed one can also think of the checking that ESC/Java does in the absence of any user annotations as simply checking implicit assertions before each pointer dereference, array access, etc., so that, for example, the program fragment
    x = a[i];
    is treated as if it were
    //@ assert a != null; assert 0 <= i; assert i < a.length;
    x = a[i];
    There are several valuable differences between the explicit introduction of assertions through the use of assert pragmas and their implicit introduction through other ESC/Java pragmas and through built-in checking rules:
  • Warnings arising from assert pragmas all produce the same kind of warning message:
    • ...: Warning: Possible assertion failure (Assert)
    Implicitly introduced assertions, on the other hand, give rise to a wide variety of more specific messages.
  • An assert pragma can occur only where a Java statement can occur, but implicitly introduced assertions are not limited to statement boundaries.  For example, given the statement
    • p = m(q) + q[++i]
    ESC/Java makes sure that the implicit assertion that array q is non-null is introduced at a control point after the call to method m, and that the implicit assertion that index i is in bounds is introduced at a control point after i is incremented.  For the user to introduce explicit assertions at these points, it would be necessary to modify the Java source code, breaking the statement into several parts and introducing a temporary variable for the result of the call to m.
  • An assert pragma introduces a single assertion at the control point where it occurs.  In contrast, a single other pragma (or built-in checking rule) can introduce many assertions throughout the program--for example, at every call of a given method, or at every access to a given variable.
  • The systematic introduction of assertions at certain points in a program sometimes makes it possible for ESC/Java safely to introduce assumption at other points.
    • In short, the various pragmas (and built-in checking rules) provided by ESC/Java enable the introduction of collections of assertions and assumptions in a manner that would be quite tedious, awkward, and error-prone to accomplish with explicit assert and assume pragmas alone.

    2.2.2  A nowarn pragma suppresses warnings by turning assertions into assumptions.

    Recall from the previous section (2.2.1) that ESC/Java's built-in checking for null dereferences works, in effect, by implicitly putting an assertion before each pointer dereference in the program, so that the line

        209:      z = x.f;

    gets treated as if it were

    209:      /*@ assert x != null; */ z = x.f;
    except that the precise text of the warning message, if any, is different.  The way that a nowarn pragma suppresses warnings is by turning the (implicit or explicit) assertions that would generate the warnings into assumptions.  Thus, for example, the code fragment
    209:      z = x.f; //@ nowarn Null;
    210:      w = x.g;
    is treated by ESC/Java like
    209:      /*@ assume x != null; */ z = x.f;
    210:      /*@ assert x != null; */ w = x.g;
    By changing the implicit assertion that x is non-null on line 209 into an assumption, the nowarn pragma not only prevents ESC/Java from warning of a possible dereference of null on line 209, but also satisfies the implicit assertion on line 210, thus preventing ESC/Java from warning that the evaluation of the expression x.g might dereference null.

    It should be clear from the above that the comments in section 2.2.0 about the need for judgment regarding the use of assume pragmas are (at least) equally applicable to nowarn pragmas.

    2.2.3  A helpful tip:  Experiments with assert and assume pragmas can help you understand ESC/Java's behavior and debug your annotated code.

    As illustrated in the example of section 0, using ESC/Java will often be an iterative process:  You run ESC/Java on your program; it reports some warnings; you address the warnings by changing either the Java code itself or the annotations; you run ESC/Java again; and so on until ESC/Java reports no warnings.  At some point in this process, you may find that you can't figure out why ESC/Java is issuing some warning, or why the change you made to address some warning isn't making the warning go away.  In such cases experiments with assert  and  assume  pragmas can be useful in the same way that displaying intermediate results is useful in ordinary debugging.

    Suppose, for example, that the problem seems to be that ESC/Java is missing some critical fact that ``should be obvious.''  You might try adding an assert pragma for the (supposedly obvious) fact and see whether ESC/Java really warns that the assert could fail.  Or you might try adding an assume pragma to see whether supplying the (supposedly critical) missing fact really eliminates the warning.

    Such experiments can also clarify your own understanding of your program.  Consider, for example, the situation described in section 0.7, where ESC/Java continued to complain of a possible array bounds error even after we fixed the bug in the surrounding for loop:

    ESC/Java input from file Bag.java:
           ...
    16:      for (int i = 0; i < n; i++) {
    17:        if (a[i] < m) {
           ...
    ESC/Java output:
    Bag.java:17: Warning: Possible array index too large (IndexTooBig)
          if (a[i] < m) {
               ^
    1 warning
    If we found this behavior puzzling we might consider the experiment of adding an  assert  pragma between lines 16 and 17.  The outcome of the experiment would depend on which of the two ``obvious'' assertions we chose:
    //@ assert i < n;
    or
    //@ assert i < a.length;
    In either case, observing the outcome might take us a step closer to understanding the situation.

    Note:  Some earlier versions of ESC/Java had a bug that sometimes resulted in highly counterintuitive failure to warn of the first potential error on an execution path.  For example, if a program contained the lines

    23:      //@ assert x < 10 & y < 10;
    ...      ...   // statements not modifying x
    33:      //@ assert x < 10;
    then ESC/Java might have produced an Assert warning for line 33, but not for line 23 (even though the assertion at line 33 could be false after execution of lines 24-32 only if the assertion at lines 23 had been false beforehand, and even though ESC/Java would have warned about line 23 if the assertion in line 33 were not present).  This behavior could be quite confusing for a user attempting to use assert pragmas as a debugging aid, as suggested in this section.  We have since made changes to ESC/Java to prevent such behavior, or at least greatly reduce its likelihood.  If you observe a case where addition of an assertion inhibits ESC/Java from warning about a potential error earlier in the execution path, we would like to know about it. See the instructions on reporting bugs in appendix B.

    2.3  Pragmas for specifying routines

    In this section, we describe those pragmas, called routine modifier pragmas,  that explicitly supply specifications for individual routines.

    Fine points

    The reader should be aware that these pragmas are not the only ones that give rise to routine specifications.  In this regard, we direct the reader's attention particularly to the descriptions of the non_null and invariant pragmas in sections 2.4.0 and 2.4.1, as well as to the description of the axiom pragma in section 2.4.2.

    All routine modifier pragmas have a number of properties in common:

    2.3.0  requires pragma

    A requires pragma is a routine modifier pragma.  It has the form
    requires E ;opt
    where E is a boolean specification expression.  The pragma makes E a precondition of the routine the pragma modifies.  When checking the body of the routine, ESC/Java assumes that E holds initially.   When checking a call to the routine, ESC/Java issues a warning if it cannot establish that E holds at the call site.

    Fine points

    If the routine is synchronized, then E is assumed to hold before acquisition of the lock.  If the routine is a constructor, then E is assumed to hold before the implicit superclass constructor call, if any, and thus also before execution of instance variable initializers.

    Except for the formal parameters of the routine, the variables mentioned in E must be spec-accessible (see section 3.3) anywhere the routine itself is accessible.  For example, a precondition of a public method may not mention a private variable (unless the variable is declared spec_public, see section 2.5.0).

    A method declaration that overrides another method declaration cannot be modified with a requires pragma, but inherits the overridden method's preconditions as described above.  Multiple inheritance can lead to unsoundness in some cases, as discussed in section C.0.5.

    A single routine declaration may be modified with any number of requires pragmas.  The effective precondition is the conjunction of all the preconditions given, but any resulting warning message indicates the specific requires pragma giving rise to the warning, and warnings arising from each pragma can be suppressed individually.

    2.3.1  modifies pragma

    A modifies pragma is a routine modifier pragma.  It has the form
    modifies L ;opt
    where L is a nonempty, comma-separated list of specification designators.  A specification designator designates a mutable component of the state.  It is very much like a Java LeftHandSide [JLS, 19.12], but generalized as described below.  The pragma specifies that the routine is allowed (but not required) to modify any of the state components listed in L.

    The state components named in modifies pragmas of a routine are called modification targets of the routine.  When checking code that calls a routine, ESC/Java assumes that the call modifies only the routine's modification targets (with the usual substitutions) and possibly also any freshly allocated state, regardless of whether the call terminates normally or abruptly. However, the current ESC/Java does not enforce modifies pragmas when checking a routine's implementation.

    Fine points

    Permissible forms of specification designators are:

    A routine may be annotated with multiple modifies pragmas, in which case a call is assumed possibly to modify any state component listed in any of the modifies pragmas.  If no modification targets are specified for a routine, then ESC/Java will assume that calls to the routine modify only freshly allocated state, if any.

    A method declaration that overrides another method declaration cannot be annotated with a modifies pragma, but inherits the modification targets of the overridden method.  Note that this forbids the overriding method from modifying additional state, but see the description of also_modifies below (section 2.3.8).

    2.3.1.0  target fields

    When a modification target of a routine has the form E.f (or simply f, meaning this.f), the field f is said to be a target field of the routine.  (Note that a modification target of the form E.g.f makes f but not g be a target field).

    2.3.2  ensures pragma

    An ensures pragma is a routine modifier pragma.  It has the form
    ensures E ;opt
    where E is a boolean specification expression.  The pragma makes E a normal (that is, non-exceptional) postcondition of the routine the pragma modifies.  When checking the body of the routine, ESC/Java issues a warning if it cannot establish that E holds whenever the routine terminates normally. When checking code that calls the routine, ESC/Java assumes that E holds just after the call if the call terminates normally.

    In a postcondition of a non-void method, the special ESC/Java identifier \result denotes the result of the method.  (For constructors, the constructed object may be denoted only by this, not by \result.) The static type of \result is the result type of the method.

    Within E, an expression of the form \fresh(R) where R is a specification expression of a reference type is true if the object denoted by R in the post-state is allocated in the post-state (implying that R != null in the post-state) and was not allocated in the pre-state.  The static type of \fresh(R) is boolean.

    A postcondition E may contain expressions of the form \old(X).  Roughly speaking, \old(X) means the value of X in the pre-state.  The static type of \old(X) is the same as the static type of X.  An expression X used as an argument of \old may not itself contain applications of \old or \fresh.  More precise details are given below.

    Fine points

    Postconditions of a synchronized method apply to the state after the release of the lock.

    Except for formal parameters, identifiers used in postconditions of a routine (and not within \old) denote their values in the post-state.  While Java allows a routine body to include assignment to the routine's formal parameters (thus using the parameters as local variables), such assignments have no effect as seen by the caller, since parameters are passed by value.  Therefore ESC/Java interprets occurrences of formal parameters in postconditions as denoting the original (pre-state) actual parameter values.

    A single routine declaration may be modified with any number of ensures pragmas.  The effective postcondition is the conjunction of all the postconditions given, but any resulting warning message indicates the specific ensures pragma giving rise to the warning, and warnings arising from each pragma can be suppressed individually.

    In a postcondition, an expression of the form \old(X), where X is a specification expression, denotes the value denoted by X, except that (1) any occurrence in X of a target field (see section 2.3.1.0) of the routine is interpreted according to the pre-state value of the field, and (2) if any modification target of the routine has the form A[i] or A[*], then all array accesses within X are interpreted according to the pre-state contents of arrays.  Note that in the normal postcondition of a non-void method, \result always refers to the method's result, even when \result occurs in an argument to \old.  Similarly occurrences of this in a normal postcondition of a constructor always refer to the constructed object.  See sections 2.3.3and 3.2.15 for further discussion of the semantics of \old.

    It is a source of potential unsoundness for a postcondition to mention a variable that might not be spec-accessible (section 3.3) to an override of that method, and ESC/Java may forbid such postconditions.  In particular ESC/Java forbids postconditions of a method that mention private variables except when the routine is static, is final, is private, or is declared in a final class, or when the private variables mentioned are declared spec_public (section 2.5.0).  The current ESC/Java doesn't forbid, for example, postconditions of public methods from mentioning package variables, but future versions of ESC/Java may not be so lenient.

    A method declaration that overrides another method declaration cannot be modified with an ensures pragma, but inherits the postconditions of the overridden method.  (See also the also_ensures pragma described in section 2.3.5.)

    Since Java guarantees that a constructor call returns a newly allocated object, ESC/Java automatically supplies the postcondition \fresh(this)for every constructor.

    2.3.3  A note on the interaction of modifies and \old

    [This section may be skipped on first reading.]

    The current ESC/Java does not check that the body of a routine actually obeys the constraint expressed by the routine's modifies pragmas.  This lack of checking is one of several potential sources of missed warnings (unsoundness).  The potential for missed warnings is mitigated somewhat by a fact that may have seemed surprising when we mentioned it in the previous section (2.3.2):  If a particular field (either a static field or an instance variable) is not specified as a target field (section 2.3.1.0) of a routine, then occurrences of that field within arguments to \old in the routine's postconditions are taken to refer to post-state values.

    Consider, for example a class with an integer field f and a method incf declared as follows, with no modifies pragma:

    //@ ensures f == \old(f) + 1;
    void incf() {
      this.f++;
    }
    Since f is not specified as a modification target of incf, ESC/Java will interpret both occurrences of f in the ensures pragma as referring to the post-state value of this.f.  Consequently ESC/Java will be unable to show that the method establishes the specified postcondition, and will issue a warning to that effect.

    While this warning may seem surprising, the result of interpreting the second occurrence of f as the pre-state value of this.f would be even worse.  Under the latter interpretation ESC/Java would issue no warnings about the body of incf, but would assume after a call x.incf() both (1)  that x.f had been incremented in accordance the postcondition), and (2) that x.f was left unchanged in accordance with the (unchecked) empty set of modification targets.  Since these assumptions are mutually contradictory, the result would be equivalent to assuming false, and ESC/Java would silently omit all checking after the call.

    As an additional guard against omission of modifies pragmas, ESC/Java issues a caution message for any occurrence of \old(X) in a postcondition of a method m unless (1) the expression X mentions some target field of m, or (2) the expression X includes an array access and m has some modification target of the form A[I] or A[*].

    Of course,  the interactions of modifies and \old described above do not entirely make up for the fact that the current ESC/Java does no checking of modifies pragmas.  A method declaration like

    //@ modifies someOtherObject.f; //instead of this.f
    //@ ensures f == \old(f) + 1;
    void incf() {
      this.f++;
    }
    can still effectively disable checking of code following calls to incf.

    2.3.4  exsures pragma

    An exsures pragma is a routine modifier pragma.  It has the form
    exsures (T t) E ;opt
    or
    exsures (T) E ;opt
    where T is a subtype of java.lang.Throwable, t (if included) is a an identifier, and E is a boolean specification expression.  The identifier t (if included) is in scope in E, where it has type T.  The pragma makes E an exceptional postcondition of the routine the pragma modifies.  That is, it specifies that E holds whenever the routine completes abruptly by throwing an exception t whose type is a subtype of T.

    When checking the body of the routine, ESC/Java checks that E holds whenever the routine completes abruptly by throwing an exception t whose type is a subtype of T.  When checking code that calls the routine, ESC/Java assumes that the E holds just after the call if the call completes abruptly with an exception whose type is a subtype of T.

    Fine points

    Like normal postconditions, exceptional postconditions of synchronized methods apply to the state after the release of the lock.

    The identifier t may not be the same as any formal parameter of the routine, and quantified expressions (see sections 3.2.10 and 3.2.11) within E may not use t as a bound variable name.

    The expression E can include uses of \fresh and \old, which have the same semantics as in an ensures pragma.  However, E cannot mention \result, since an abruptly-terminating routine invocation returns no result.  Similarly E cannot mention this if the exsures pragma modifies a constructor, since we take the view that the object being constructed should be discarded.  (This view is potentially unsound; see section C.0.8.)

    A single routine declaration may be modified with any number of exsures pragmas.  ESC/Java checks that the body obeys each exsures pragma and assumes that calls obey each exsures pragma.  For example, if a routine is modified by the pragmas

    exsures (T1 t) E1; exsures (T2 t) E2;
    where T2 is a subtype of T1, then ESC/Java checks (if checking the body of the routine) or assumes (if checking a caller) that E1 holds whenever the routine completes abruptly by throwing an exception that is an instance of T1,  and that both E1 and E2 hold whenever the routine completes abruptly by throwing an exception that is an instance of T2.

    A method declaration that overrides another method declaration cannot be modified with an exsures pragma, but inherits the exceptional postconditions of the overridden method.  (See also the also_exsures pragma described in section 2.3.6.)

    2.3.5  also_ensures pragma

    An also_ensures pragma is a routine modifier pragma.  It has the form
    also_ensures E ;opt
    where E is a boolean specification expression.  An also_ensures pragma has the same semantics as an ensures pragma, but may appear as a modifier only of a method declaration that overrides another method declaration (while overriding method declarations are forbidden to have ensures pragmas).

    2.3.6  also_exsures pragma

    An also_exsures pragma is a routine modifier pragma.  It has the form
    also_exsures (T t) E ;opt
    or
    also_exsures (T t) E ;opt
    where T is a subtype of java.lang.Throwable, t (if included) is a an identifier, and E is a boolean specification expression.  An also_exsures pragma has the same semantics, and must obey the same syntactic restrictions, as an exsures pragma, but may appear as a modifier only of a method declaration that overrides another method declaration (while overriding method declarations are forbidden to have exsures pragmas).

    The relationship between also_exsures and exsures is exactly analogous to that between also_ensures and ensures.

    2.3.7  also_requires pragma

    An also_requires pragma is a routine modifier pragma.  It has the form
    also_requires E ;opt
    where E is a boolean specification expression.  An also_requires pragma has the same semantics as a requires pragma, but the declaration of a method C.m may be modified by an also_requires pragma only if all three of the following conditions hold: (By contrast, a requires pragma may only modify a method [or constructor] declarations that does not override any other method declaration, and neither a requires pragma nor an also_requires pragma may modify a method declarations in classes that overridden declaration in a superclasses, or a method declaration in an interface that overrides a method declaration in a superinterface.)

    Fine points

    The also_require pragma is a potential source of unsoundness.  Suppose method C.m of class C overrides method I.m of interface I.  When checking a