Trustworthy Tools
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support

A Mechanically Verified
Verification Condition Generator


Sunrise is a system for proving programs correct in a feasible way. It contains a deep embedding of a small programming language within the HOL theorem prover, and provides a tool, called a verification condition generator or VCG, for the semi-automatic creation of proofs of partial or total correctness for Sunrise programs within HOL. The VCG is itself verified as sound, and that soundness proof is contained within and checked by the HOL system. This permits the significant simplification of proofs of partial or total correctness of Sunrise programs while retaining complete security.

The programming language supported by Sunrise is a normal imperative language, containing assignments, conditionals, and 'while' commands, and also mutually recursive procedures, with both variable and value parameters. All variables have the type of natural numbers.

The verification condition generator reduces the problem of proving the correctness of a program with respect to its specification to a set of verification conditions which only deal with the underlying data types of the variables in the language. In particular, all iterative or recursive reasoning with respect to proving the correctness of loops or of recursive procedures is resolved by the VCG, automatically, and does not appear in the verification conditions produced.


The most important new feature, introduced in version 7.1, is the support for proving either the partial or total correctness of commands and programs, where the old version supported only total correctness. This facilitates the use of Sunrise in the classroom, where the instructor may wish to first teach about partial correctness, and later show how the termination arguments can be added to prove total correctness. It would also aid in the industrial proof of an algorithm's correctness, beginning with partial and progressing to total correctness when and if desired for the project. This provides a two-step spectrum of correctness strength, with the stronger result requiring additional specification and proof.

In addition, error messages are now provided to aid in the diagnosing of programs which are not well-formed. As a small improvement, multiple variables may now be bound by a single quantifier.

A teacher may wish to introduce the Floyd/Hoare-logic axioms and rules for the while-language subset first, and give exercises for proving the partial correctness of commands, and then subsequently add the rules for specifying procedure declarations and calls. Later the instructor can introduce the more sophisticated rules for specifying and proving the total correctness of loops and mutually recursive procedures.


Here is the source code for Sunrise version 7.4. It is compatible with the Higher Order Logic theorem prover, HOL4 version Kananaskis-4 and later.

For HOL4 versions Kananaskis-1 through Kananaskis-3, please use Sunrise version 7.3.


After downloading Sunrise version 7.4, install it as follows, where {HOLDIR} stands for the root directory of the HOL4 system.

mv vcg-74.tar.gz {HOLDIR}/examples
cd {HOLDIR}/examples
gunzip vcg-74.tar.gz
tar xvf vcg-74.tar

This will create a new subdirectory called sunrise in the {HOLDIR}/examples directory. Then to build the Sunrise system, type

cd sunrise/src

To load the Sunrise system into an HOL4 session, type the following lines:

loadPath := HOLDIR ^ "/examples/sunrise/src" :: !loadPath;

load "vcg_parser";
open vcg_parser;

load "vcg_prettyp";

load "vcg_tactics";
open vcg_tactics;

If you also wish to use the fast but insecure tactics, type

load "fvcg_tactics";
open fvcg_tactics;

All of the above steps for loading Sunrise, and some additional tools, may be loaded by entering the single line

use (HOLDIR ^ "/examples/sunrise/examples/load_vcg.sml");

There are a collection of example programs in the {HOLDIR}/examples/sunrise/examples directory. Try them by starting HOL4 in that directory, and then typing

use "ex1.sml";

for the first example, so on for examples 2 through 8.

Previous Versions

The prior version of Sunrise (from July 2005) is version 7.3, used with HOL 4, versions Kananaskis-1 through Kananaskis-3.

Version 7.2 of Sunrise (released January 2004) is used with HOL 4, versions Kananaskis-1 and Kananaskis-2. Version 7.2 was corrected to compensate for the time bug in Moscow ML which manifested in January 2004.

Version 7.1 of Sunrise (released June 2002) is used with HOL 4, version Kananaskis-1. (Make sure you have installed the fix for the time bug in Moscow ML.)

Version 7.0.1 of Sunrise (released June 2002) is used with HOL 98, version Taupo-5 or Taupo-6.

Version 7.0.1 supports proving the total correctness of either commands without procedure calls, or entire programs with mutually recursive procedures. It also introduced the additional feature of uninterpreted function symbols.

Please note these versions of Sunrise will not build with version Hol98 Taupo-4 or earlier, or with Hol90 or Hol88.

NOTE: To build Sunrise versions BEFORE 7.3 under Windows, one (empty) folder needs to be added after unpacking the above archive. Before typing "Holmake" to build Sunrise as described in the installation instructions, in the {HOLDIR}\examples\sunrise folder, create the new (empty) folder "listings". This will hold listings of each of the theories created when Holmake builds Sunrise. For the standard installation of HOL, the new directory will be

C:\Program Files\Hol\examples\sunrise\listings

This step is not needed under UNIX.

Versions before 7.0

5.1, 6.1, 6.2, and 6.3 of Sunrise are available for downloading. They are used with versions of HOL 90, as described below.

These are uuencoded, gzipped tar archives. Unpack them using uudecode, gunzip, and tar in the HOL "contrib" directory, for example by:
gunzip sunrise6.3.tar.gz
tar xvf sunrise6.3.tar
This creates a single directory called "vcg" in the contrib directory. Directions for making the library are included in the README file in vcg.

These versions of the Sunrise system correspond to different versions of the HOL theorem prover:

HOL version Sunrise version
HOL88 v. 2.02 Sunrise v. 5.1
HOL90 v. 7 or
HOL90 v. pre9
Sunrise v. 6.0
Sunrise v. 6.1
Sunrise v. 6.2
HOL90 v. 10 Sunrise v. 6.3
HOL98 v. Taupo-5 or -6 Sunrise v. 7.0.1
HOL 4 v. Kananaskis-1 Sunrise v. 7.1
Sunrise v. 7.2

Version 7.0.1 introduced the additional feature of uninterpreted function symbols. Version 7.1 introduced support for partial correctness as well as total correctness, and also provided error messages to help diagnose programs which are not well-formed. Version 7.2 compensated for a bug in Moscow ML which manifested in January 2004. These three versions are also the only ones with a User's Guide (PDF).

For versions 6.3 and before, despite the increase in version number and the change to being based on HOL90 instead of HOL88, all these versions are logically and functionally almost identical. Other than some minor syntax changes, the major difference is in speed; the functions that apply the VCG to a given Sunrise program to securely construct a proof of its correctness have been substantially rewritten, with improved timing results.

Here is an additional example, with its results, as described in the paper for TPHOLs'98. This was not included in the set supplied with the libraries above.

Please see the papers above for more documentation.

Making formal methods into normal methods.