Tools for SPARK Proof
There are two tools available: VC_View and PCHIF.
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.
In version 2.0 of VC_View the user can subset the user identifiers that determine the hypotheses to tbe shown.
VC_View 2.0 can be downloaded from the Download page.
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.
Version 2.02 is now available separately and is included in the download archives.
This release has a bug fix for incorrect responses to prompts and is updated to work with the new version of the Proof Checker included in the SPARK Pro release (Checker Version 8.1.0).