HOL-Boogie

Complex specifications can pose a challenge for VCC. By means of the HOL-Boogie plugin in VCC, such specifications can be exported to the interactive theorem prover Isabelle to be inspected and proved correct.

We demonstrate the usage of HOL-Boogie on the following example, which we assume to be stored in file simple.c:

#include "vcc.h"

int simple(int i)
  ensures(i == result)
{
  return 1; // fails for i != 1
} 

Exporting a problem to HOL-Boogie

To inspect or verify the example in HOL-Boogie, it needs to be exported (or translated). The following command accomplishes just that:

vcc /b:/prover:Isabelle /b:/proverOpt:ISABELLE_INPUT=simple.b2i simple.c 

In the output, VCC will report

Verification of simple was inconclusive. 

which should not be taken as an error: instead of verifying the example, we only used VCC to export the corresponding verification condition. Consequently, VCC cannot report validity (or a counterexample); the actual inspection and verification is performed in HOL-Boogie.

Using HOL-Boogie

To use HOL-Boogie, first start Isabelle with a new theory file Simple.thy:

isabelle emacs -l HOL-Boogie Simple.thy

As a starting point, the following skeleton may be used, where <PROOF> specifies the place to the yet-to-be-found proof of correctness for our example.

theory Simple
imports Boogie
begin

boogie_open simple

boogie_vc simple <PROOF>

boogie_end

end

The command boogie_open loads the translated program into HOL-Boogie, the command boogie_vc selects a verification condition to be proved, and the command boogie_end ends verification (and checks if all verification conditions have been proved).

The typical proof attempt (replacing <PROOF> above) looks as follows:

proof (split_vc (verbose) try: smt)

This method splits the verification condition into splinters and tries to automatically discharge them. Those splinters for which this method fails stay for manual inspection. Each splinter corresponds to an assertion in the C program (the proposition to be proved) along with a trace to the program up to the location of this assertion (serving as assumptions for the proposition).

Not surprisingly, in the case of the considered example, HOL-Boogie reports that the assertion at line 4 (the postcondition) cannot be proved.

When changing the return statement in the example to return i, the example can be proved correct. In this case, the placeholder <PROOF> may be replaced by

  unfolding labels
  by (smt boogie)

Further examples demonstrating HOL-Boogie can be found in the Isabelle sources.

Last edited Feb 22, 2010 at 2:39 PM by stobies, version 5

Comments

No comments yet.