Re: The future of Spark . Spark 2014 : a wreckage

[Stefan.Lucks@uni-weimar.de]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1783 bytes --]

On Wed, 10 Jul 2013, Randy Brukardt wrote:

>> Secondly, Ada's "in", "out", and "in out" information give only a cursory
>> view of what is going on.
>
> Of course. But that and the postcondition is all you ought to be depending
> upon. If you're depending on more, your program is more fragile than it
> ought to be.

Your program can depend on whatever has been specified (and hopefully 
proven) in the specification. Which is one reason why "Depends" is 
actually useful -- you are allowed to make more specific contracts.

> ... (detailed and possibly interesting examples of Depends removed)
>
> ...
>> Without "Depends", your cool analysis tool verifying all pre- and
>> postconditions will not catch this bug.
>
> Sure, but so what? It's a fools game to try to catch all bugs, it not even a
> worthwhile goal. (That's essentially where Spark goes wrong, in my view.)

Who said, catch all bugs? I didn't.

> What I care about is extending what Ada already does well: catch the
> low-hanging fruit of bugs.

By my own experience, having worked occasionally with SPARK, information 
flow analysis actually catches a lot of errors -- even without having 
specified any pre- or postconditions. In other words, SPARK's information 
flow analysis actually gives you the low-hanging fruits you mention.

The fruits (well, bugs) you catch by employing pre- and postconditions are 
a bit higher, actually. At least, that is what I gather from my own 
experience YMMV. Did you ever actually work with SPARK?

So long

Stefan


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
     <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--