* 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