A couple of tools for SPARK Proof

A couple of tools for SPARK Proof

[JP Thornley]

I've developed a couple of tools to help when doing Spark proof - called 
VC_View and PCHIF.

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

1. Only immediately relevant hypotheses are initially shown
2. User identifiers are replaced by upper case letters

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

Other features allow the hypotheses to be restricted to just those for a 
single conclusion, and give access to the rules file for the VCs.


The main purposes of PCHIF are to make it easier to recall and edit 
previously entered commands and to give better control over the commands 
that are stored.

As well as making it easier to create proof scripts, PCHIF should also 
simplify the creation of 'clean' scripts - i.e. ones without failed 
inferences, etc. (A long term ambition for PCHIF is to simplify the 
maintenance of proof scripts by providing a 'stop on fail' feature - to 
make it easier to pinpoint commands that need changing.)

At present PCHIF is an experimental prototype and has a number of 
limitations - the main one is that it only handles input to the Checker.
(In order to handle the output from the Checker it must be piped to 
another program - when this is done the Checker prompts don't appear 
down the pipe until after the Checker has received the input that it is 
prompting for.)

Both tools are 100% Ada, and compiled with GNAT 3.15p. Only MS Windows 
executables are provided (XP Pro, but may work on other versions). 
However they use GtkAda so it should be possible to compile them for 
other platforms. (The sources aren't currently provided for download but 
I intend to make them available once they've been made fit for public 
view.)

The download page can be reached from www.sparksure.com.

If you try the tools, please use the contact email address given on the 
sparksure pages to send me comments.

Cheers,

Phil Thornley
-- 
JP Thornley