DirectVCGenExplanation

WikiInclude(DirectVCGenDescription)

The Mobius Direct VC Generator is called ``direct'' because, contrary to the other verification condition generators of the PVE, it uses a simple weakest precondition calculi without any use of an intermediate language. The source VC generator is written in Java and the bytecode VC generator is written in Coq. It is part of the proof transforming compiler scheme, as explained in the deliverable 4.3 [wiki:Bibliography (MobiusDeliverable4.3).

One of the main goals of this tool is to translate the proofs for the verification conditions generated from the source code to proofs for the verification conditions generated from the bytecode. Therefore, both VC generation subsystems have to be reasonably similar, to allow this transformation. Both weakest precondition calculi have exactly the same set of rules. The only thing that differs between the two calculi is their way of handling variables. Of course, bytecode variables can be easily programatically deduced from the source code ones.

The background predicates for both verification conditions are found in the same theory, that of \bicolano. The tool Bico is used to translate a program into the Coq formalization. The backend for the VC generator over source code is a specific Coq backend that uses Bicolano as its memory model.

Version: 1 Time: Thu Mar 27 17:14:45 2008 Author: dcochran (dcochran) IP: 193.1.132.32