The Compaq Extended Static Checker for Java (ESC/Java), developed at the Compaq Systems Research Center (SRC), is a programming tool for finding errors in Java programs. ESC/Java detects, at compile time, common programming errors that ordinarily are not detected until run time, and sometimes not even then; for example, null dereference errors, array bounds errors, type cast errors, and race conditions.
ESC/Java2 is now available from Nijmegan University. It handles later versions of Java and JML than the original SRC tool. Here is a link to its homepage. More information about ESC/Java2 is available in recent papers about JML.
ESC/Java uses program verification technology, but feels to a programmer more like a type checker. By using an underlying automatic theorem prover, ESC/Java is more semantically thorough than decidable static analysis techniques. At the same time, because it tries to detect certain kinds of errors only, and not prove the program's correctness, the technique is more automatic than full functional program verification.
ESC/Java includes an annotation language with which programmers can express design decisions using light-weight specifications. For example, one may give a method precondition that says that a parameter is not null, or declare an object invariant that says that an integer field lies between 0 and the length of some array field. ESC/Java uses the given annotations in reducing spurious warnings, and also checks that the program is consistent with the given annotations.
Because it uses specifications to reason about calls, ESC/Java performs modular checking. That is, ESC/Java checks each class (indeed, each single routine) separately. This means that ESC/Java can be applied to code that calls libraries even if the code for the libraries is not available. It also means that ESC/Java can be applied to library code whose clients or subclasses have not yet been written.
ESC/Java is available for download for research and educational use. In fact, we are quite excited about the prospect of ESC/Java being used in education. We speculate that students using ESC/Java as part of programming classes will develop a practical understanding of important programming concepts such as invariants and preconditions, because ESC/Java provides instant feedback just like typecheckers and parsers do. We hope to help instructors use ESC/Java in teaching by allowing them to share their experiences and programming assignments with other instructors.
Legal Statement Privacy Statement