Re: SPARK Proof - Tutorials and Tools

["Michael" <fvit@shaw.ca>]

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/