|
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/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.
The system includes an annotation language that extends Java to include such things as pre- and post-conditions and invariants.
Posted to Software-Eng by Ehud Lamm on 3/9/01; 7:28:28 AM
|
|
Extended Static Checking for Java
