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.

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

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.