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.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin2!goblin.stu.neva.ru!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: Wed, 10 Jul 2013 18:10:15 -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 1373497820 15849 69.95.181.76 (10 Jul 2013 23:10:20 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 10 Jul 2013 23:10:20 +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: 4979 Xref: number.nntp.dca.giganews.com comp.lang.ada:182448 Date: 2013-07-10T18:10:15-05:00 List-Id: wrote in message news:alpine.DEB.2.10.1307100904530.27942@debian... On Tue, 9 Jul 2013, Randy Brukardt wrote: > wrote: >>> So you think, information flow analysis is completely worthless? (I >>> mean, >>> for building and verifying correct systems -- as a compiler writer you >>> will not question the usage of information flow analysis inside the >>> compiler or optimiser). >> >> Information flow *within* a subprogram is important. Information flow >> *between* subprograms is completely defined by the subprogram's >> interfaces >> and calls. > >Firstly, for current Ada (i.e., Ada 2012) this is completely wrong >whenever a program manipulates global variables. Even specifying pre- and >postconditions doesn't guarantee the absence of any other (side-)effects. >(You are right, however, a proper "global" annotation would seem to catch >this.) I'm always presuming a proper globals annotation. You really can't do anything without it (Janus/Ada does almost no optimizations across subprogram calls precisely because Ada doesn't have this information in its contracts). >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. ... (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.) If you had some magic annotations that could specify a totally bug-free program, then there no longer is any need for the program at all. Just execute the annotations, and forget the error-prone Ada code! What I care about is extending what Ada already does well: catch the low-hanging fruit of bugs. There are always going to be a few really tough bugs that aren't going to be detectable automatically -- the goal should be to reduce that number in practical programs (no matter how large), not to eliminate all bugs in a barely usable subset of tiny programs. Think about all of the "bugs" that we Ada programmers don't really have to deal with, because the compiler or runtime has already automatically detected it. That's not just type errors and array indexes out of range, but also dereferencing null pointers, accessing the wrong variant in a record, and many more. (I don't think Janus/Ada would have ever worked reliably without the variant check -- the early versions always had weird stability problems that disappeared as soon as we implemented the variant checks [and spent months eliminating all of the errors that turned up]). What I think is important is bringing that level of ability to user-defined properties (think Is_Open and Mode for Text_IO files), and detecting more of these problems at compile-time (which is always better then runtime). It's not being able to detect every possible bug. My main point is that I think people are trying to solve the wrong problem, and that leads to having over-elaborate contracts. >I agree that no one should depend on what the body of some Subprogram >does. But then, information flow analysis is actually useful! ...in very marginal cases. I don't think it's worth trying to cover every possible base, certainly not before compilers even do a passible job on the easy cases. Once every Ada compiler does basic proof using pre/post/globals/exception contracts, we can revisit. Randy.