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!feeder.eternal-september.org!gegeweb.org!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Thu, 20 Aug 2015 15:36:06 -0500 Organization: JSA Research & Innovation Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1440102968 12745 24.196.82.226 (20 Aug 2015 20:36:08 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 20 Aug 2015 20:36:08 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:27535 Date: 2015-08-20T15:36:06-05:00 List-Id: "Shark8" wrote in message news:9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com... ... > As others have said, SPARK is about avoiding exceptions completely > (because > the relevant properties are proved) and therefore having exceptions in > your SPARK > code is not allowed. One use of exceptions is to signal errors with the parameters of a routine -- essentially the failure of a precondition. Clearly, it is better that such things are proved impossible, and thus such exceptions are not needed in SPARK. But another use of exceptions is to signal things that cannot be known at compile time. How can you tell in advance whether the file Foobar.Txt exists on your disk? Even a pretesting it is unreliable (it could be deleted between the test and the usage); one has to report the error at runtime. SPARK forces such errors to be reported as error codes, and that's pure evil. The problems with using error codes rather than exceptions to report unlikely but possible errors are well-known, and forcing one to use that is essentially junking decades of programming experience. The lack of access types is similar; one has to emulate them using arrays in SPARK, which is a 1950s programming technique. It's the sort of thing that one uses Ada to get way from. At least the SPARK team is aware of these limitations and considering ways to mitigate them in future versions of SPARK. What I hate is people spinning these as "features" rather than just a limitation of prover technology (and to me, an indication that SPARK tries to do too much). Randy.