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----