From: Stefan.Lucks@uni-weimar.de
Subject: Re: Problems with SPARK 2015 and XMLAda
Date: Fri, 21 Aug 2015 08:26:53 +0200
Date: 2015-08-21T08:26:53+02:00 [thread overview]
Message-ID: <alpine.DEB.2.20.1508210804480.22981@debian> (raw)
In-Reply-To: <mr5dnn$ce9$1@loke.gir.dk>
[-- Attachment #1: Type: text/plain, Size: 3080 bytes --]
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
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
allow error codes, the caller cannot ignore the error and still prove its
own postconditions (at least for any sort of useful postconditions).
The weak case is about readability. It is a reason why error codes are
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
often better readable than programs where the error-handlers are
distributed across the source code, with an error handler after every
program call returning an error code.
> 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.
Agreed!
Unfortunately, the state of static verification in general is that proving
properties for pointer-hopping programs is almost hopeless. There is some
recent work in this direction, e.g., by Bertrand Mayer, but this only goes
so far.
> 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
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
technologies. Which is actually quite cool.
Actually, you can use access types in SPARK programs, as long as you
encapsulate them away from the prover. Encapsulating access types is what
you have proposed in another thread, actually.
More precisely, you can write SPARK specifications (no access types!)
claiming postconditions, exception freedom and the like, for your
subprograms. Now you implement your packages/subprograms in pure Ada (no
SPARK) with access types used internally, if needed. The correctness of
such packages is an unproven assumption. But can "with" your subprograms
in your own SPARK bodies.
If you stick to your promises (your postconditions hold if the
preconditions are statisfied), i.e., if the unproven assumptions are
correct, then the full program is correct.
Of course, you would like to prove *everything* -- at least, I would like
to do so. But mixing full Ada with SPARK is, IMHO, the best approach to
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-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----
next prev parent reply other threads:[~2015-08-21 6:26 UTC|newest]
Thread overview: 25+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-08-19 15:58 Problems with SPARK 2015 and XMLAda Serge Robyns
2015-08-19 20:21 ` Simon Wright
2015-08-19 21:22 ` Serge Robyns
2015-08-20 7:10 ` Jacob Sparre Andersen
2015-08-20 10:06 ` Mark Lorenzen
2015-08-20 16:38 ` Shark8
2015-08-20 18:42 ` Peter Chapin
2015-08-20 19:13 ` Jeffrey R. Carter
2015-08-20 20:00 ` Serge Robyns
2015-08-20 20:36 ` Randy Brukardt
2015-08-20 23:21 ` Shark8
2015-08-21 6:26 ` Stefan.Lucks [this message]
2015-08-21 7:30 ` Dmitry A. Kazakov
2015-08-21 8:19 ` Stefan.Lucks
2015-08-21 9:37 ` Dmitry A. Kazakov
2015-08-21 10:09 ` G.B.
2015-08-21 11:56 ` Dmitry A. Kazakov
2015-08-21 13:46 ` G.B.
2015-08-21 14:45 ` brbarkstrom
2015-08-21 15:34 ` Dmitry A. Kazakov
2015-08-21 23:44 ` Bob Duff
2015-08-22 6:22 ` Dmitry A. Kazakov
2015-08-21 10:43 ` Stefan.Lucks
2015-08-21 12:35 ` Dmitry A. Kazakov
2015-08-24 21:32 ` Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox