ANN: SPARK Proof - Tutorials and Tools

ANN: SPARK Proof - Tutorials and Tools

[JP Thornley]

I have put a couple of tutorials on SPARK proof onto www.sparksure.com; 
one for proof of absence of run-time error (ie using the optional proof 
annotations) and one for using the Proof Checker. Both tutorials contain 
several sections, with worked examples and exercises.

I have also updated a couple of tools that help with SPARK proof:
1) VC_View makes it easier to read and interpret SPARK verification 
conditions.
2) PCHIF is an interface to the Proof Checker that makes it easier to 
recall and edit previously entered commands and to control the commands 
that are saved.
(Previous versions of PCHIF were very unstable, but this is now sorted, 
thanks to Dmitry Kazakov and Maxim Reznik for their Gtk Router.)

The tutorials and the tools (Windows executables only at present) can be 
downloaded from www.sparksure.com.

Phil Thornley
phil at sparksure dot com
-- 
JP Thornley

Re: ANN: SPARK Proof - Tutorials and Tools

[John McCormick]

Phil,

Thanks for the examples.  There are too few available for folks who
want to see what they look like.  I'm looking forward to going through
your tutorials.

John

Re: SPARK Proof - Tutorials and Tools

[Michael]

Thank you Phil,

It is the best documentation and "how to use guide" ever made on this 
subject.



That is a long overdue and great clarification on the SPARK purpose, 
constraints and limitations.

(i.e.: Proof of Absence of Run-time Error).



"The Simplifier does not prove all provable Verification Conditions (a 
provable VC is one where the conclusions can be shown to be logical 
consequences of the hypotheses). Any VCs remaining after simplification may 
be provable (but beyond the capability of the Simplifier to prove) or 
unprovable."



That's start to make sense.



Mathematical approximations sometimes don't deal easily with computer 
calculation errors.

I was assuming that is a flight trajectory/airspace intersection instability 
risk that SPARK or Praxis's Correctness by construction can't easily 
evaluate.



I think that shall confirm SPARK as one programming insurance tool (doing it 
right), and don't compromise the use of Ada like a Computer Assisted 
Engineering tool (doing the right thing).



Now, about knowing what we are doing, did you suggest the proof must be 
elaborated once the functional behaviour has been thoroughly tested (unit, 
non-regression, integration, verification, (validation) testing - all the 
kit indeed)?

i.e.: "Proof Checker, (This option may lead to proofs that are difficult to 
maintain.)"



Indeed, that is what could have prevented the Praxis's iFACTS project from 
entering the wall.  (see above for a plausible explanation)



And about project as complex and big than iFACTS, (I have another similar in 
mind, and mind a responsible answer) would you suggest SPARK could still be 
an affordable option, e.g.: taking into account the overhead that 
annotations and proofs shall require (quite twice of the project's level of 
effort, as I would figure - learning curve not entirely included)



Cheers,



Michael,

Vancouver, British Columbia



Praxis's Tokeneer demo is also available - example is still instructive, but 
SPARK usage and limitations are poorly documented:

http://www.adacore.com/home/products/gnatpro/tokeneer/

Re: ANN: SPARK Proof - Tutorials and Tools

[Tim Rowe]

JP Thornley wrote:
> I have put a couple of tutorials on SPARK proof onto www.sparksure.com; 
> one for proof of absence of run-time error (ie using the optional proof 
> annotations) and one for using the Proof Checker. Both tutorials contain 
> several sections, with worked examples and exercises.

A bit of nostalgia for me there! I did the PVL SPADE course about 19 
years ago, but hardly used it because my employer at the time turned out 
not to have a lot of application for it. A lot of SPARK seems oddly 
familiar :-)