From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,121ed47e1e990d4d X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news2.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!newsfe20.iad.POSTED!7564ea0f!not-for-mail From: "Michael" Newsgroups: comp.lang.ada References: Subject: Re: SPARK Proof - Tutorials and Tools X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5512 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 X-RFC2646: Format=Flowed; Response Message-ID: NNTP-Posting-Host: 174.6.150.104 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: newsfe20.iad 1237820145 174.6.150.104 (Mon, 23 Mar 2009 14:55:45 UTC) NNTP-Posting-Date: Mon, 23 Mar 2009 14:55:45 UTC Date: Mon, 23 Mar 2009 07:55:41 -0700 Xref: g2news2.google.com comp.lang.ada:5206 Date: 2009-03-23T07:55:41-07:00 List-Id: 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/