ESCJava2Explanation

WikiInclude(ESCJava2Description)

The Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts to find common run-time errors in JML-annotated Java programs by static analysis of the program code and its formal annotations. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with specially formatted comments called pragmas. It supports multiple Theorem Provers.

ESC/Java2 is a large-scale subsystem within the PVE. Its architecture relies upon several of the other subsystems described in this document including the original DEC-SRC Java frontend (Javafe) and the Simplify theorem prover, both of which are described in this section, and several other new Mobius subsystems, most of which are described in this wiki.

In a nutshell, ESC/Java2 translates JML-annotated java source code into verification conditions that are passed to an automated theorem prover. Responses from the prover are translated back into informational messages useful to a normal programmer.

To implement these features, ESCJava2 uses a combination of Javafe to lex and parse Java sourcecode, an internal bytecode subsystem to parse Java bytecode, and its own JML lexer and parser, all of which produce a JML-annotated Java AST. This representation is then translated into a semantically equivalent guarded command, dynamic single assignment-based representation, which is then used to generate a verification condition with either a weakest precondition or a strongest postcondition VC generator. This VC is represented in one of two forms, the original DEC-SRC VC AST, or the new Mobius sorted VC AST. This VC is passed to an automated theorem prover via one of two mechanisms, either the original DEC-SRC Simplify-specific interface, or the new Mobius automated prover backend. Likewise, responses from the automated prover flow back through these same interfaces.

In summary, ESC/Java2 uses more Mobius subsystems than any other component, except the PVE itself. It represents the core system used to perform research on, and evolve existing, generic verification functionality, as well as exercise and extend various other PVE subsystems.

Version: 5 Time: Thu Mar 27 18:01:01 2008 Author: dcochran (dcochran) IP: 193.1.132.32