* ANN: SPARK Proof - Tutorials and Tools @ 2009-03-19 12:13 JP Thornley 2009-03-20 16:31 ` John McCormick ` (2 more replies) 0 siblings, 3 replies; 4+ messages in thread From: JP Thornley @ 2009-03-19 12:13 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: ANN: SPARK Proof - Tutorials and Tools 2009-03-19 12:13 ANN: SPARK Proof - Tutorials and Tools JP Thornley @ 2009-03-20 16:31 ` John McCormick 2009-03-23 14:55 ` Michael 2009-03-23 19:38 ` ANN: " Tim Rowe 2 siblings, 0 replies; 4+ messages in thread From: John McCormick @ 2009-03-20 16:31 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: SPARK Proof - Tutorials and Tools 2009-03-19 12:13 ANN: SPARK Proof - Tutorials and Tools JP Thornley 2009-03-20 16:31 ` John McCormick @ 2009-03-23 14:55 ` Michael 2009-03-23 19:38 ` ANN: " Tim Rowe 2 siblings, 0 replies; 4+ messages in thread From: Michael @ 2009-03-23 14:55 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: ANN: SPARK Proof - Tutorials and Tools 2009-03-19 12:13 ANN: SPARK Proof - Tutorials and Tools JP Thornley 2009-03-20 16:31 ` John McCormick 2009-03-23 14:55 ` Michael @ 2009-03-23 19:38 ` Tim Rowe 2 siblings, 0 replies; 4+ messages in thread From: Tim Rowe @ 2009-03-23 19:38 UTC (permalink / raw) 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 :-) ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2009-03-23 19:38 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2009-03-19 12:13 ANN: SPARK Proof - Tutorials and Tools JP Thornley 2009-03-20 16:31 ` John McCormick 2009-03-23 14:55 ` Michael 2009-03-23 19:38 ` ANN: " Tim Rowe
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox