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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: "Jeffrey R. Carter" Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Thu, 20 Aug 2015 12:13:47 -0700 Organization: Also freenews.netfront.net; news.tornevall.net; news.eternal-september.org Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 7bit Injection-Date: Thu, 20 Aug 2015 19:12:06 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="ee44d3db9c41f5ad88d7e8e8f0268f05"; logging-data="7935"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19DrYHDJ8G/jgnfNCVIyGBSOeqg7FMXQos=" User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0 In-Reply-To: Cancel-Lock: sha1:KsJN1zrNknSjgn84N2CjaK+e5ZQ= X-Enigmail-Draft-Status: N1110 Xref: news.eternal-september.org comp.lang.ada:27532 Date: 2015-08-20T12:13:47-07:00 List-Id: On 08/20/2015 11:42 AM, Peter Chapin wrote: > > To clarify, SPARK 2014 does allow raise statements in programs. However, each > Raise statement carries with it a proof obligation that it will never execute. > What's the point of that? It allows you to use raise statements to document > "impossible" situations and then have the tools attempt to prove that those > situations are, indeed, impossible. SPARK is usually discussed in the context of complete programs, in which you prove both that a subprogram is correct if the caller meets the precondition, and that all calls meet the precondition. However, in the case of a library unit that may be called by multiple programs, it may be desirable to be able to prove the correctness of the unit without being able to prove that all calls will be correct. In such cases, having assertion checking catch the precondition violation and raise an exception is the best solution should the unit be misused. Also, some preconditions are very expensive to check; consider the "N is prime" example discussed here in another thread. In such a case, it may be that the normal processing allows detecting a precondition violation much more cheaply than checking the precondition at the time of the call. In that case, a conditional raise statement, which the condition being provably false if the precondition is met. Then the unit can be proven correct if the precondition is met, execute without the expensive precondition check in the case where the call is not proven correct, and still raise an exception if it is called with the precondition not met. So it does seem there are cases where this feature may be useful. -- Jeff Carter "I've seen projects fail miserably for blindly applying the Agile catechism: we're Agile, we don't need to stop and think, we just go ahead and code!" Bertrand Meyer 150