- ESC/Java
is a checker for Java programs, optionally annotated with user-supplied
pragmas.
- ESC/Java
pragmas must occur within pragma-containing comments.
We showed some examples of pragma-containing comments in section
0. Section
2 includes all
the rules about where the various kinds of pragmas are allowed.
- ESC/Java
pragmas can contain expressions that are similar to Java expressions.
The ESC/Java specification language--that is, the language of
ESC/Java pragmas--includes expressions, which we call specification
expressions, or SpecExpr's. While the syntax,
name-resolution,
and type-checking rules for specification expressions are similar to
those
for
ordinary Java expressions, there are inevitably some differences.
The rules for specification expressions are described in section
3 of this manual.
- ESC/Java
pragmas record programmer design decisions.
In addition to giving the user control over ESC/Java, pragmas serve
to record formally some of the programmer's intentions about the
function
and use of methods, constructors, and variables (for example, that the
Bag
constructor of our example in section
0 was meant never to be called with a null argument).
These
are the same sorts of intentions that good programmers may already
record
informally in natural language comments.
- ESC/Java's
pragmas support modular checking.
The checking done by ESC/Java is modular. When checking
the body of a routine (that is, a method or constructor) r,
ESC/Java does not examine bodies of routines called by r.
Rather, it relies on the specifications of those routines, as
expressed
by requires pragmas, by other pragmas described below, and by
Java constructs such as signatures, return types, and throws
clauses.
Conversely, to check the body of r, ESC/Java does not examine
callers of r. It does, however, assume that r
is
called only in accordance with its own specification.
- When
Java sources are unavailable, users can supply pragmas in .spec files.
When the file declaring a class T uses a type U,
ESC/Java may need data invariants of U and/or specifications
of
U's
routines in order to check the routines of T. If
ESC/Java
can find only a binary (.class) file and no source file
declaring
U,
then it will assume simple default specifications for the routines of U
based on their signatures. The user can supply additional
specifications
for the routines of U, and also invariants for
U, by
putting them in pragmas in a file U.spec. A .spec
file is like a .java file except that it is allowed to omit
method
bodies. Section
5.1 tells more about .spec files.
Section
2 includes descriptions of all
ESC/Java pragmas.
- ESC/Java
is checker for (almost all of) Java 1.2.
ESC/Java is targeted for Java 1.2, as described in The Java
Specification
Language, by James Gosling, Bill Joy, and Guy Steele [JLS],
supplemented by the ``Inner Classes Specification'' [ICS],
except for some limitations described in section
6 of this manual.
- ESC/Java
has a command-line interface like the Java compiler's.
An invocation of ESC/Java has the form:
escjava
[
options
] sourcefiles
The escjava(1) man page in the ESC/Java release (see appendix
B) includes descriptions of ESC/Java's command-line options and of
environment variables that affect ESC/Java's operation. For now
we
mention only the CLASSPATH environment variable, whose effect
on ESC/Java is similar to its effect on javac(5) and the -suggest
command-line option, which causes ESC/Java to offer suggestions of
pragmas
that might eliminate certain kinds of warnings. Section
5 contains further description of these features (but not all
command-line
options and environment variables).
- ESC/Java
issues warning messages for potential run-time errors.
- The
current ESC/Java checks only method and constructor bodies.
The current ESC/Java provides no warnings for potential run-time errors
in static initializers [JLS, 8.5] or in initializers for static
fields or in anonymous classes.
- ESC/Java
treats exceptions thrown by the Java run-time system as run-time errors.
Some of the potential ``error'' conditions detected by ESC/Java are
conditions that would be detected by the Java run-time system and give
rise to exceptions (specifically, NullPointerException,
IndexOutOfBoundsException,
ClassCastException,
ArrayStoreException, ArithmeticException, and NegativeArraySizeException
[JLS, 11.5.1.1]). The current ESC/Java treats these
conditions
as errors, and generates warnings for them even if the program actually
catches the resulting exceptions. Accordingly, our use of the
word
``error'' in this manual includes such conditions. Future
versions
of ESC/Java may provide support for checking programs that catch
exceptions
thrown by the Java run-time system. The current ESC/Java
version
does support checking of programs that catch explicitly-thrown
exceptions
(including those just listed).
- ESC/Java
does not warn of potential errors in the evaluation of specification
expressions.
Specification expressions are never actually evaluated, and (with one
exception described in section
2.6.1)
ESC/Java will not produce specific warnings about specifications
expressions
whose evaluation might dereference null, access arrays out of
bounds, etc. Rather, the meanings of such expressions (for
example,
O.f
where O , if it were actually evaluated, might
evaluate
to null) are an unspecified function of (the meanings of)
their
subexpressions. In most cases, attempts to prove things about
such
unspecified values will fail, thus giving rise to warnings of some sort
(though alas not the clearest warnings that one could hope for).
- ESC/Java
warning messages may include execution traces.
Associated with each ESC/Java warning message is some execution path
that--so far as ESC/Java can determine--may plausibly lead to the
run-time
error mentioned in the warning. If certain kinds of
``interesting''
events occur on this execution path, the message will contain an execution
trace listing those events. See
section
4.0 for details about which events are considered ``interesting''.
Section
4 of this manual includes descriptions
of all ESC/Java warning messages.
- ESC/Java
issues error messages for badly formed programs.
Before ESC/Java can analyze a program for potential run-time errors,
it must first perform operations such as parsing, name resolution, and
type-checking both of the Java code and of any pragmas. When
ESC/Java
detects an illegal construct (such as the syntactically incorrect
pragma
shown in section
0.8 above) during this preliminary processing, it issues an error
message. Error messages are distinguished from warning messages
by
the occurrence of the word Error instead of Warning
near the beginning of the message. Only when its input is free of
such errors can ESC/Java go on to look for potential run-time errors
and
generate warnings (just as a compiler generates object code only when
the
source code is free of compile-time errors).
- ESC/Java
error messages are like compiler error messages.
ESC/Java error messages are similar to compiler error messages, and
we hope they will be self-explanatory. Thus, they are not fully
enumerated
or described in this manual. We believe that all ESC/Java error
messages
arise either (1) from circumstances that would cause the Java compilers
to report compile-time errors or (2) from violations of the rules for
writing
pragmas as given in section
2 and section
3.
- ESC/Java
doesn't detect all compile-time errors that Java compilers detect.
A number of conditions that give rise to Java compile-time errors are
not detected by ESC/Java. For example, the current ESC/Java does
not enforce Java's definite assignment rules [JLS, 16] or all of
Java's restrictions on access to protected variables [JLS,
6.6.2]. Thus it is wise to run your code through a Java compiler
at least once before trying to run it through ESC/Java. (Tip:
Sometimes the nature of a syntax error in your program may not be
immediately
clear from an ESC/Java error message. In such cases, a compiler
may
detect the same error and offer a better--or at least
different--description
of the problem.)
- ESC/Java's
extended static checking isn't perfect.
- ESC/Java can miss
errors.
When ESC/Java processes a program and produces no warnings, it is not
necessarily true that the program is free of all errors. For
example,
ESC/Java never checks for some kinds of errors, such as arithmetic
overflow,
or infinite looping. Also ESC/Java doesn't check programs for
functional
correctness properties other than those given by the user in
pragmas.
Finally, even when ESC/Java checks for a particular kind of errors,
there
may be situations in which it erroneously concludes that the error
cannot
occur, and therefore fails to issue a legitimate warnings. In the
jargon of proof theory, we say that ESC/Java--viewed as a system for
proving
program correctness--is unsound. Section
C.0 describes the known sources of unsoundness in ESC/Java.
- ESC/Java
can give
spurious warnings.
Conversely, when ESC/Java issues a warning, it doesn't necessarily
indicate the presence of an error; it merely means that ESC/Java is
unable
to conclude that the indicated error will never occur, given the
annotations
that the user has supplied. In the jargon, ESC/Java--viewed as a
system for proving program correctness--is incomplete. Section
C.1 describes the main sources of incompleteness in ESC/Java.
- Pragmas
give the user some control over ESC/Java's unsoundness and
incompleteness.
ESC/Java provides pragmas that let the user eliminate spurious
warnings--that
is, reduce ESC/Java's incompleteness--either without loss of soundness
(as, for example, the
requires pragma we wrote in section
0.2 eliminated the warning about a potential dereference of null
in the Bag constructor by imposing a precondition on calls)
or,
if need be, at some risk of lost soundness (as in the case of the nowarn,
assume,
and axiom pragmas respectively described in sections
2.1.0,
2.1.2,
and 2.4.2
below).
- ESC/Java
issues caution messages in some (but not all) cases where
unsound
checking may occur.