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: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!gegeweb.org!news.ecp.fr!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: Fri, 12 Jul 2013 15:47:40 -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 1373662062 22307 69.95.181.76 (12 Jul 2013 20:47:42 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 12 Jul 2013 20:47:42 +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 Xref: news.eternal-september.org comp.lang.ada:16333 Date: 2013-07-12T15:47:40-05:00 List-Id: wrote in message news:alpine.DEB.2.10.1307120950410.10151@debian... On Thu, 11 Jul 2013, Randy Brukardt wrote: >>> 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. > >Firstly, whatever data flow annotations are, they are not "junk". > >Secondly, there is no "giant pile" of data flow annotations. Actually, >they usually take a lot less lines of "anno-code" than writing pre- and >postconditions. So even if you consider the data flow annotations as >redundant, their overhead is small. I called them "junk" because they're redundant (certainly in well-designed code). The OP complained that the proposed annotations for Spark 2014, and I agree with him on that. But I find it irrelevant because they're redundant. And I'm strongly opposed to putting redundant information in specifications or anywhere else. I've learned by painful experience over the years that redundant information -- in type declarations, a compiler symboltable, or a programming language standard -- always ends up out of sync with the original infomation. That's especially true if it cannot be automatically checked (I'm dubious that "Depends" could be checked that way given the information available to an Ada compiler). So, I want to eliminate as much as possible of that information. Clearly, we're not getting rid of parameter modes. Clearly, we need preconditions and postconditions, they can't be done any other way. That makes "Depends" the redundant information that we should not have in a specification. Moreover, I really don't see what value they could possibly have. A subprogram has a number of "in" parameters and a number of "out" parameters (and possibly, but hopefully not some input globals and output globals, and treating a function result as a "out" parameter for this discussion). All of the "in" parameters should somehow effect the "out" parameters (and it is best if there is only one output). Routines that don't have this structure are already dubious. It sometimes can't be avoided, but it should be extremely rare. So, already, the extra information gained by this "flow" information is minimal. On top of that, "out" parameters that don't depend on some parameters are likely to be obvious in the postcondition for that parameter. The point is that there isn't much information to be gained from such an annotation; the vast majority of it is repeating the obvious (inputs affect outputs). I realize that there are a lot of badly designed subprograms out there, but I wouldn't want a significant language feature just for badly designed subprograms -- especially when we still need lots of support for *well* designed subprograms! ... >> Your experience seems to have been on annotating existing code, > >Not at all! (Well, I tried once to SPARKify existing Ada code -- but I got >rid of that disease very very quickly. Turning naturally-written Ada into >proper SPARK is a pain in the you-know-where!) The reason I said that if you design new code, you write the preconditions and postconditions along with the subprogram specification (many in the form of predicates, I would hope, as those are a lot easier than repeating large pre- and post-). (And you surely don't write subprograms where only some of the inputs affect some of the outputs.) Before you write anything else (like bodies or even descriptions of the purpose of the routine). I've never heard of any experienced Ada programmer writing subprogram specifications without considering the proper subtypes of the parameters immediately! So I don't see how you could get just "Depends" annotations. I grant that you might "beef up" the preconditions and postconditions later, to provide a more complete description, but you're almost always going to start with some. >One real life example (simplified for the purpose of posting this) is the >implementation an authenticated encryption scheme. Consider two byte >strings X and Y of the same length, X being the message and being Y the >"key stream". There is additional authentication key K. The output of the >authenticated encryption is the ciphertext (X xor Y), followed by a >cryptographic checksum(*) of X under the key K. This sounds like precisely the bad sort of subprogram that typically should be avoided. Multiple outputs, and a strange non-dependence of some of the outputs on some of the inputs. I grant this can be unavoidable in some cases, but it should be rare. I don't see any point of an annotation that only provides extra information for such rare cases. Probably a more sensible annotation here would be the negative: that is, declare which inputs a particular output does *not* depend upon. That normally should be a null list, in the rare case where it is non-null the information could be given. But, as I said, this is not information useful to an Ada compiler (while the other annotations will improve code quality). Randy.