ProofPower |
ProofPower is a specification and proof tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm, in Standard ML. ProofPower provides support for specification and proof in Z using a semantic embedding of Z into HOL. The DAZ tool supporting refinement of Z to the SPARK subset of Ada is also available.
ProofPower was developed under a collaborative project involving ICL, PVL and the Unversities of Cambridge and Kent, which ran from 1990 through to the end of 1992.
During 1993 and 1994 support for Z and Ada was included and work
on the software has continued from 1994 to the time of writing
(2011/02/01 17:24:37).
ProofPower is currently tested by Lemma 1 Ltd. on x86 architectures
running Linux, Mac OS X, OpenSolaris and Cygwin.
The ProofPower X Windows interface package PPXpp uses OpenMotif (not available
on Cygwin).
The Standard ML components of ProofPower can be compiled using either Poly/ML
or Standard ML of New Jersey.
See the read-me file for more details.
Proofs in Z are intended to be conducted with all visible subgoals
in Z (though an extended dialect of Z). In practice, this is usually the case.
However we do not at present attempt to teach use of the tool for Z without
first teaching HOL.
The language supported is an approximation to `ISO standard Z' rather
than the Z of Mike Spivey's `Z: A Reference Manual'.
The source file formats use either an extended character set or
an ASCII mark-up. These two formats are interconvertible using
tools supplied with the PPTex package.
The ASCII mark-up is similar in spirit to the
e-mail mark-up of the ISO Standard, but not in the details.
There is no automatic way of transferring specifications
between the ProofPower dialect of Z and other Z support tools at the moment.
Now the standard has been finalised we hope that there will be more convergence.
There are no standards in place or in prospect for Higher Order Logic.
The variant of the logic implemented in ProofPower is identical to that
supported by the Cambridge HOL system (HOL88) and other HOL systems at an
abstract level, though the concrete syntax used differs from that used in other
HOL systems. In practice this means that specifications will be intelligible
to people familiar with Cambridge HOL but that there is currently no automatic transfer
of either specifications or proofs between the two environments.
Work on interchange between HOL systems is under way, but in its early stages at the moment.
The best self-training material to start with is derived on two short courses covering ProofPower-HOL and
ProofPower-Z.
The course material is available in transparency format
(HOL,
Z) and as tutorial notes
(HOL,
Z).
The Z course assumes you are familiar with the material in the HOL course.
You will almost certainly want to use the X Windows interface xpp when you work through the course,
so before you start you may like to look at the
Xpp User Guide.
Full documentation is obtainable from the
ProofPower Web site.
WHAT IS THE CURRENT STATUS of ProofPower?
WHAT SOFTWARE AND HARDWARE DO I NEED to run ProofPower?
DOES ProofPower COMPLETELY HIDE THE UNDERLYING HOL WHEN WORKING IN Z?
IS ProofPower COMPATIBLE WITH OTHER Z TOOLS?
IS ProofPower COMPATIBLE WITH OTHER HOL TOOLS?
WHERE DO I START TO LEARN HOW TO USE ProofPower?
HOW DO I GET MORE INFORMATION ABOUT ProofPower?
|
|