ANN: SPARK Proof Libraries
Phil Thornley
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
Peter C. Chapin
> 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.
I haven't looked at your tool yet (I will download it now), but in
general I think this is a great idea.
Peter
Shark8
a modular type of mod 3 which is flatly disallowed in SPARK. ;)
[/horrible-pun]