Extended Static Checking for Java (ESC/Java)

Weihan Huang





1.    What “Extended static checking” means.


Extended mean that ESC catches more errors than are caught by conventional static checkers such as type checkers.


Static means that the checking is performed without running the program.




2.    Features of ESC/Java


ESC/Java is powered by verification condition generation and automatic theorem proving. It examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotation and the actual code.


It performs Modular checking, i.e. it operates on one piece (a method or a constructor) of the code at a time




3.    Architecture


ESC first produces Abstract Syntax Trees from Annotated Java program, and then translates it to Guarded commands, and then generate verification conditions (VC_R). Then VC_R and Type specific Background knowledge (BP_T) which are all expressed in FOPC are given to the Theorem prover with the conjecture

          UBP and BP_T => VC_R

where UBP is the universal background predicate which encodes some general facts about the semantics of Java. Finally the post-processor produces warnings according to the theorem prover results.



4.    Annotation Language


Basically, ESC/Java uses annotation //@ comments with a method. This annotation serves to states a method’s object invariant, routine specifications (pre-condition, post-conditions) as follows.


1.     Annotations appear like other Java declarations, modifiers or statements, but encoded in Java comments that begin with an @-sign. expressions contained in annotations are side-effect free java expressions, with a few additional keywords and functions.


2.     Two abstract variables are declared as "fields" of each object type: valid and state. x.valid means the object x satisfies the internal invariant of x's type. and  x.state represents the abstratc state of the object x.


3.  Routine specifications can contain any or all of the following parts :

       requires P : precondition

       modifies M : a list of lvalues modified

       ensures Q : post-condition

       exsures R : exceptional post condition

    Overriding methods inherit specifications from the methods they override. Users may also strengthen the post-conditions of the overrides using also_ensures and also_exsures.


4. ESC also provides ghost fields, which are like ordinary fields in Java, except that the compiler does not see them. A Common use of ghost fields is to make up for the absence of generic types in Java. Such as to require the elements of a vector of some specified type.