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!newsfeed.fsmpi.rwth-aachen.de!newsfeed.straub-nv.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: Problems with SPARK 2015 and XMLAda Date: Fri, 21 Aug 2015 08:26:53 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <6952b70d-a9bc-4d0a-beb5-1cd38d6a3318@googlegroups.com> <9d3dc132-4e1a-4e9c-bcd4-82a42a73745f@googlegroups.com> NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: multipart/mixed; BOUNDARY="8323329-770196924-1440138415=:22981" X-Trace: pinkpiglet.scc.uni-weimar.de 1440138998 21262 141.54.178.228 (21 Aug 2015 06:36:38 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Fri, 21 Aug 2015 06:36:38 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.20 (DEB 67 2015-01-07) Xref: news.eternal-september.org comp.lang.ada:27541 Date: 2015-08-21T08:26:53+02:00 List-Id: --8323329-770196924-1440138415=:22981 Content-Type: text/plain; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Thu, 20 Aug 2015, Randy Brukardt wrote: > SPARK forces such errors to be reported as error codes, and that's pure > evil. There are two cases against error codes, a strong one and a weak one. The strong case that programmers just tend to forget handling them, or=20 even intentionally ignore them. This is why error codes are evil. But this is a non-issue for SPARK: If the postconditions of a subprogramm= =20 allow error codes, the caller cannot ignore the error and still prove its= =20 own postconditions (at least for any sort of useful postconditions). The weak case is about readability. It is a reason why error codes are=20 bad, but not quite evil. And it actually is an issue for SPARK: Source code with well-used exception handlers at the bottom of a block are= =20 often better readable than programs where the error-handlers are=20 distributed across the source code, with an error handler after every=20 program call returning an error code. > The lack of access types is similar; one has to emulate them using=20 > arrays in SPARK, which is a 1950s programming technique. It's the sort=20 > of thing that one uses Ada to get way from. Agreed! Unfortunately, the state of static verification in general is that proving= =20 properties for pointer-hopping programs is almost hopeless. There is some= =20 recent work in this direction, e.g., by Bertrand Mayer, but this only goes= =20 so far. > At least the SPARK team is aware of these limitations and considering=20 > ways to mitigate them in future versions of SPARK. What I hate is people= =20 > spinning these as "features" rather than just a limitation of prover=20 > technology Agreed! > (and to me, an indication that SPARK tries to do too much). SPARK tries to do as much as possible with current static verification=20 technologies. Which is actually quite cool. Actually, you can use access types in SPARK programs, as long as you=20 encapsulate them away from the prover. Encapsulating access types is what= =20 you have proposed in another thread, actually. More precisely, you can write SPARK specifications (no access types!)=20 claiming postconditions, exception freedom and the like, for your=20 subprograms. Now you implement your packages/subprograms in pure Ada (no=20 SPARK) with access types used internally, if needed. The correctness of=20 such packages is an unproven assumption. But can "with" your subprograms=20 in your own SPARK bodies. If you stick to your promises (your postconditions hold if the=20 preconditions are statisfied), i.e., if the unproven assumptions are=20 correct, then the full program is correct. Of course, you would like to prove *everything* -- at least, I would like= =20 to do so. But mixing full Ada with SPARK is, IMHO, the best approach to=20 provably correct programs possible with today's technology. Stefan -------- I love the taste of Cryptanalysis in the morning! -------= - www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-luck= s ----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany-= --- --8323329-770196924-1440138415=:22981--