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
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.
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.
boogie_vc simple <PROOF>
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
by (smt boogie)
Further examples demonstrating HOL-Boogie can be found in the Isabelle sources