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: border1.nntp.ams3.giganews.com!border2.nntp.ams3.giganews.com!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!newsfeed.fsmpi.rwth-aachen.de!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: The future of Spark . Spark 2014 : a wreckage Date: Thu, 11 Jul 2013 19:21:16 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373588477 31702 69.95.181.76 (12 Jul 2013 00:21:17 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 12 Jul 2013 00:21:17 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-Original-Bytes: 4128 Xref: number.nntp.dca.giganews.com comp.lang.ada:182479 Date: 2013-07-11T19:21:16-05:00 List-Id: 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.