Authors: Cormac Flanagan, K.M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe and Raymie Stata
This paper presents a program verification tool: ESC/Java. The philosophy behinds the extended static checking is letting programmers provide information to help the static verification processes. The method they used is designing an annotation language, similar to Java comments, to describe the behaviors of objects and methods, and using theorem prover to find bugs. The advantages of writing annotation as comment are not affecting compiler and providing "good" comments.
The goals of ESC/Java are statically verifying some important correctness properties, and giving warnings to "missing comment" and "inaccurate comment". It also wants to reduce the cost of correcting errors and provide flexibility for programmers. As a result, it is neither sound (all errors will be reported) nor complete (all reported errors are real errors, not false alarms). The design of annotation language is toward Java-like and lightweight spec. Several trade offs of language design are considered: missed errors, spurious warnings, annotation overhead and performance.
The architecture of ESC/Java includes front end, translator, verification commands generator, theorem prover and postprocessor. The Front End gets annotated Java program and produces abstract syntax trees (AST) and type-specify background predicate (used for theorem prover). The Translator translates routine calls to guarded commands (GC), which gives each command preconditions. The VC Generator generates predicates form guarded commands. The Theorem Prover (Simpler) uses UBP (universal background predicate) and BP (background predicate of a class definition) to verify VC (verification conditions). The Postprocessor produces warnings when VCs are not provable. The counterexamples for warnings are also generated by "Simplify" and represented as labels.
The annotation language for routine specifications includes require P, modify M, ensure Q and exsure (T x) R. Requires P specifies pre-conditions of the methods; Modifies M is a list of variables (objects) to be modified; Ensures Q states post- conditions for the method; Exsures (T x) R is for exceptions. The overriding methods in sub-typing objects use Also_* to annotate. For multiple inheritance, by interface, ESC/Java uses union to combine the inherited annotations.
ESC/Java mainly uses object invariance, like non_null or requires, verifying the correctness of object. The invariance of an object bounded to the operations (methods) of the object. Other functions outside the object can use the modifier "helper", but it is expensive. The invariance enforcement on the call sites only applies to the static field and arguments. The placement of invariance is not restricted either. Some methods, like constructor, are even not required to satisfy the invariance.
ESC/Java also uses data abstraction in some way, called ghost field. The ghost fields are like fields of an object, but invisible for compiler. It is only for checker. The common use of ghost field is for the absence of generic types of Java. We can restrict the type of elements in some generic data structures, like vector, to be the same.
To provide flexibility and avoid complicated situations, ESC/Java has escape hatches in annotation language, like nowarn and assume. Nowarn turns off specific warning and Assume make an assumption for variables. Although these escape hatches make unsoundness and incompleteness, they are necessary and can avoid specification creep.
The unsoundness and incompleteness of ESC/Java also come from other ways. First, it only performs modular checking, which is according to the specification of routine call, not the real code of the routine. Second, it does not check arithmetic overflow checking. Third, the invariance of loops is obtained by unrolling them a fixed number of times, not find real fixed points. The number of unrolling times is configurable by programmer, which provides the flexibility to control the trade offs between accuracy and efficiency. The last one comes from the partial enforcement of object invariance.
The performance of ESC/Java can be measured in two aspects: cost for finding bugs and annotation overhead. Theorem prover is the main performance cost for ESC/Java. For a large Java program, most errors can be identified within a "reasonable" time (5min). The annotation overhead is around 40-100 annotation/KLOC in average. The effort of annotation can be reduced by annotation inference or some assistant tools, like Houdini.
The other claims in their conclusion include (1) machine checkable code helps maintenance. (2) ESC/Java can detect the violation of design decision, such as protocol errors. (3) ESC/Java is suitable for use in a classroom. The feature works include reducing spurious warning and lowering the perceived annotation burden.