ANN: SPARK Proof Libraries

[Phil Thornley <phil.jpthornley@gmail.com>]

The SPARK Simplifier requires all user written proof rules to be
available in files within the directory structures generated by the
Examiner.

If these directories are used for the long-term storage of user rules
then the contents and locations of the rule files are dictated by the
details of particular verification conditions rather then by the rules
themselves.  Consequently related rules become scattered over a number
of rule files, which makes them difficult to identify and more
laborious to validate.

As a first attempt at improving support for the creation and
validation of user rules and to allow all the files in the
verification directories of the Examiner and Simplifier to be deleted
and recreated, I have come up with the idea of proof libraries and a
tool - SPARKRules - that implements that idea.

An initial draft of these ideas and a prototype implementation of
SPARKRules (for Windows only) is contained in:
http://sparksure.com/resources/SPARK_Proof_Library.zip

The archive also has a sample proof library containing all the user
rules and review proofs in version 2 of the Tokeneer software and
instructions on using SPARKRules to recreate all the files required
for the proof of the Tokeneer software from this library.

All comments and queries on both the idea and the tool are welcomed.
The email address is in the archive.

Cheers

Phil Thornley