|
Abstract
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.
Papers
-
Trustworthy Tools for Trustworthy Programs:
A Verified Verification Condition Generator.
(PDF)
Peter V. Homeier and David F. Martin.
Proceedings of the 7th International Workshop
on Higher Order Logic Theorem Proving and its Applications,
eds. Thomas Melham and Juanito Camilleri, Valletta, Malta,
September 19-22, 1994, Lecture Notes in Computer Science Vol 859,
Springer-Verlag, pages 269-284.
-
Trustworthy Tools for Trustworthy Programs:
A Mechanically Verified Verification Condition Generator
for the Total Correctness of Procedures. (Ph.D. Dissertation)
Peter V. Homeier.
Department of Computer Science, University of California,
Los Angeles, June 1995.
-
A Mechanically Verified Verification Condition Generator.
(PDF)
Peter V. Homeier and David F. Martin.
The Computer Journal,
Vol. 38, No. 2, July 1995, pages 131-141.
-
Mechanical Verification of Mutually Recursive Procedures.
(PDF)
Peter V. Homeier and David F. Martin.
Proceedings of the 13th International Conference
on Automated Deduction (CADE-13),
eds. M. A. McRobbie and J. K. Slaney,
Rutgers University, New Brunswick, NJ, USA,
July 30-August 3, 1996,
Lecture Notes in Artificial Intelligence Vol 1104,
Springer-Verlag, pages 201-215.
-
Mechanical Verification of Total Correctness
Through Diversion Verification Conditions.
(PDF)
Peter V. Homeier and David F. Martin.
Accepted at
Eleventh International Conference on
Theorem Proving in Higher Order Logics (TPHOLs'98),
The Australian National University (ANU),
Canberra, Australia,
September 28 - October 1, 1998.
This will be published by Springer-Verlag in a volume of
Lecture Notes in Computer Science.
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.
Software
Installation
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
Holmake
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:
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.
|
