ProofPower `Frequently Asked Questions'
[ProofPower Logo]

ProofPower


The ProofPower FAQ

WHAT IS 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.

WHAT IS THE CURRENT STATUS of ProofPower?

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

WHAT SOFTWARE AND HARDWARE DO I NEED to run ProofPower?

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.

DOES ProofPower COMPLETELY HIDE THE UNDERLYING HOL WHEN WORKING IN Z?

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.

IS ProofPower COMPATIBLE WITH OTHER Z TOOLS?

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.

IS ProofPower COMPATIBLE WITH OTHER HOL TOOLS?

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.

WHERE DO I START TO LEARN HOW TO USE ProofPower?

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.

HOW DO I GET MORE INFORMATION ABOUT ProofPower?

Full documentation is obtainable from the ProofPower Web site.


Copyright © Lemma 1 Ltd.
Created by  Rob Arthan [rda at lemma-one dot com]
Last updated: 2011/02/01 17:24:37
[ProofPower Logo]