Independent SPARK Support

Tools for SPARK Proof

There are three tools available: SPARKRules, VC_View, and PCHIF.

SPARKRules

SPARKRules is a utility program for managing proof libraries - which can contain user rule files and proof review files.

SPARKRules allows user rules to be defined once and copied to Simplifier user rule files as required and supports the storage of proof review files in a separate library.

The directories generated by the Examiner for the Simplifier are therefore not required for the storage of any permanent data.

Version 1.0 of SPARKRules can be downloaded from the Download page.

VC_View

The purpose of VC_View is to make it easier to read and interpret Spark VCs. It does this in two main ways:

  • Only immediately relevant hypotheses are initially shown.
  • User defined identifiers are replaced by upper case letters.

The hypotheses that are shown initially are those that share a user identifier with a conclusion.
These can be selectively extended.

From version 2.0 of VC_View the user is able to subset the user identifiers that determine the hypotheses to tbe shown.

VC_View 2.1.1 can be downloaded from the Download page.

A source distribution for VC_View 2.1.1 that works on both Windows and Linux is included.

PCHIF

PCHIF is an interface to the SPADE Proof Checker.

The main purposes of PCHIF are:

  • Make it easier to recall and edit previously entered commands.
  • Give better control over the commands that are saved for a proof session.

These make it much easier to create 'clean' proof scripts - eg without failed inferences etc. - and to maintain proof scripts when changes are required.

Version 2.0 of PCHIF appears stable and reliable - earlier problems with using GtkAda on Windows have now been resolved. PCHIF version 2.03 can be downloaded from the Download page.

Problem with Proof Checker GPL version 2010

PCHIF does not operate correctly with the version of the Proof Checker included in the SPARK GPL 2010 release (see PCHIF User Manual).  The simplest way to use PCHIF with this release is to rename this Proof Checker and to copy the Proof Checker from the earlier 8.1.1 release into SPARK/2010/bin.