# 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.