SPARK Proof Libraries

I am at best a flaky Ada programmer, and my knowledge of SPARK equals more or less zero, meaning I’m having a very hard time evaluating the ideas and concepts behind Phil Thornley’s new SPARK Proof Library (zip file).

You can read the full release announcement here and a quote here:

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.

Sounds nifty!

Leave a Reply