ANN: SPARK Proof Libraries

4 views
Skip to first unread message

Phil Thornley

unread,
Nov 29, 2010, 7:09:03 AM11/29/10
to
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

Peter C. Chapin

unread,
Nov 29, 2010, 5:47:19 PM11/29/10
to
On 2010-11-29 07:09, Phil Thornley wrote:

> 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

unread,
Dec 3, 2010, 12:57:17 AM12/3/10
to
If you want your library to be SPARK-proof then I would suggest using
a modular type of mod 3 which is flatly disallowed in SPARK. ;)
[/horrible-pun]
Reply all
Reply to author
Forward
0 new messages