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

["Randy Brukardt" <randy@rrsoftware.com>]

<Stefan.Lucks@uni-weimar.de> wrote in message 
news:alpine.DEB.2.10.1307112112110.8707@debian...
On Wed, 10 Jul 2013, Randy Brukardt wrote:

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

You want to catch this very unlikely bug, and add a giant pile of extra junk 
annotations for this purpose. My contention is that it won't catch enough 
bugs by itself to be worth the complication.

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

Preconditions (and constraints) come first. You write them before you write 
any bodies, before you write any comments even - they're an integral part of 
the specification of a subprogram. So the situation you speak of isn't even 
possible.

Moreover, the vast majority of the information in "Depends" is already in 
the Ada subprogram specification (once you include its pre and 
postconditions). The question is how much it adds to already properly 
annotated subprograms, not what happens when the tools are misused.

I don't care at all about "after-the-fact" addition of these things. Hardly 
anyone is going to be adding annotations to existing packages (it's not 
clear whether we're ever going to do that for the language-defined 
packages).

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

Your experience seems to have been on annotating existing code, and doing it 
backwards ("depends" first). I can see why you might have annotated existing 
code that way, but that's not a goal or concern of mine. I'm only interested 
in new code, and code that's written properly (that is, the parameter modes 
tell one the data flow).

>Did you ever actually work with SPARK?

No, there wasn't a free version when I was interested. And now that there is 
a free version, I'm no longer interested because it is too restricted to be 
useful in any of my code. And it tries to do too much as well.

                                     Randy.