ESCJava2VCGenExplanation

WikiInclude(ESCJava2VCGenDescription)

ESCJava2 produces a VC by processing one of two input ASTs, either the GC or the DSA form, and producing one of two VC ASTs, either the original DEC-SRC ESCJava ad hoc VC AST, or the Mobius sorted AST.

VCgen is accomplished using either a weakest precondition or a strongest postcondition calculus. These calculi are discussed in detail in (ChalinHK05).

The original ESCJava VC generator focused on produced VCs describing common programming errors like null pointer exceptions and indexing an array out of bounds. The updated VC generator found in ESCJava2 also produces VCs describing proper use of constructs found in JML that did not exist in the original pragma language of ESCJava like model fields.

The background theory of the original VC generator is expressed in the concrete syntax of Simplify, within the built-in theory of Simplify. The background theory of the experimental ESCJava VC generator is expressed in several concrete syntaxes in several logics, including those of Coq, PVS, Simplify, and the SMT format.

Because of this multi-prover nature, the new VC generator is prover-independent, insofar as it generates a VC in the generic representation of the Mobius VC AST, which is, in turn, pretty-printed in a theory- and prover-aware fashion.

Version: 2 Time: Thu Mar 27 17:42:51 2008 Author: dcochran (dcochran) IP: 193.1.132.32