Sunrise

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

Welcome to the Sunrise home page, describing the research on mechanically verified verification condition generators underway in the Penn Department of Computer and Information Science, as well as pointers to related material.

Software

Current Version

The latest version of Sunrise (as of February 2005) is version 7.3, used with HOL 4, versions Kananaskis-1 through Kananaskis-3, which can be downloaded here. Sunrise is described in the Sunrise User's Guide, in either postscript or PDF.

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.

An example of using Sunrise is here.

Previous Versions

The prior version of Sunrise (from January 2004) is version 7.2, 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.

PATCH for version 7.0, as of June 2002: If you are currently using Sunrise version 7.0, then you do not need to download and rebuild the entire version 7.0.1 system. Instead, you may download the following two source files as replacements for the corresponding files in Sunrise version 7.0: Constr.sig, Constr.sml. Use these to replace the corresponding files in the vcg/src directory, and then in that directory, build the system with "Holmake" as described below.

If you download and install the above version 7.0.1, then you do not need to apply the two replacement files; version 7.0.1 already includes them.

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.

Installation

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

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

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

cd sunrise/src
Holmake
To load the Sunrise system into an HOL 4 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.

Comments are always welcome! See the documentation for the email address.

Old Versions

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:

          uudecode sunrise6.3.tar.gz.uu
          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 below for more documentation.

Other Tools

Here are new HOL tools to ease using mutually recursive datatypes and conditional rewriting.

The author appreciates all comments.

People

Papers

Related Sites on HOL