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!mx05.eternal-september.org!feeder.eternal-september.org!nuzba.szn.dk!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: SPARK Question Date: Mon, 20 May 2013 18:40:51 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <0efb385b-279a-49b7-8289-86b0e99e7930@googlegroups.com> <5188b317$0$6555$9b4e6d93@newsspool4.arcor-online.net> <68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1369093252 16568 69.95.181.76 (20 May 2013 23:40:52 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Mon, 20 May 2013 23:40:52 +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:15625 Date: 2013-05-20T18:40:51-05:00 List-Id: wrote in message news:68e3b5b0-db45-4aeb-b6c4-817fe6845e5e@googlegroups.com... On Tuesday, 7 May 2013 21:44:12 UTC+1, Randy Brukardt wrote: ... >> Similarly, postconditions often include conditions that hold true after >> the >> call, and it's quite common for those conditions to feed into following >> preconditions (as in Post => Is_Open(File) after a call to Open). So, as >> much as possible, postconditions should use the same functions that are >> used >> in preconditions. (The more that's done, the more likely that the >> compiler >> can completely eliminate the pre- and post- condition checks even when >> they're turned on.) >Addressing the last paragraph above, the basis of the point is that reusing >the >same syntactic form of predicate in pre- and postconditions makes it easy >for a >compiler to spot that a predicate is a consequence of an earlier predicate. >I >certainly agree with that! But surely this would allow only the >_subsequent_ >occurrences of the predicate to be optimized out? Above, you seem to >suggest >that both the initial and subsequent occurrence of a predicate can be >optimized out. You're right that only the "subsequent" occurrences can be optimized out - but, in well-designed abstractions, the initial state also has a well-known set of predicates. This might be hard to model in Ada 2012, although invariants certainly would help. Starting out with undefined properties is not a good idea, so the only issue is whether there is a clear way to communicate that. For instance, a file starts out with Is_Open = False. The compiler and static analyzer need to know this! It's too late to wait until Open is called. > In the example above example, it may be possible for the initial > occurrence, > the postcondition Is_Open(File) of subprogram Open, to be optimized out > but that is surely for different reasons - the compiler having special > knowledge > about the subprogram Open. Postconditions get optimized out based on the actual contents of the body. This sort of optimization should be trivial (it is made with complete knowledge of the implementation, presuming the implementation is contained in a single package body, which normally should be the case). At the call site, they're assumptions (they've either been checked or proved, either way you don't need to recheck them). > In general, for user-defined subprograms, determining statically whether a > predicate P(X) holds is, in general, difficult. Once established, it is > straightforward to use the theorem P(X) ? P(X) > to establish that subsequent occurrences of the same form hold. It's certainly true "in general", where predicate contents include functions with and depending on side-effects, where the initial state of objects is not defined, where privacy is not used properly. But why should we care about the optimization and performance of poorly designed software? > Separately, even when reusing the same syntactic form of predicate in > pre- and postconditions, optimizing out subsequent occurrences of the > predicate may not be possible as often as one would hope. Given two > occurrences of the predicate P(X), to establish that the subsequent > occurrence holds, it necessary (for the theorem above) to establish that > the X is the same in both occurrences. In the case that X is visible > outside its package and between the two occurrences of P(X) there is > a call to a subprogram in another package, I can't see how a compiler > would know that X won't be changed. (I'm assuming that compilers > don't look at the bodies of other packages when compiling a package.) > To avoid such issues, formal methods tools typically require > subprograms to have a 'frame' annotation that indicates which variables > a subprogram may change. First of all, compilers do this all the time. Any compiler that takes advantage of 10.2.1(18/3) [and most do] have been doing this for many years. In addition, this is essentially the same problem as identifying common subexpressions, a problem that optimizers have been doing since the beginning of (computer) time. So there is absolutely nothing new here. (The only part of this that would be new in Janus/Ada is the idea of assumptions, and that fits in very well with our existing optimization technology.) Secondly, one hopes that most that "predicates" are good, that is that they don't violate the Implementation Permission 11.4.2(27/3). One also hopes that most objects are of private types and are not modified "out-of-band" (whether this is possible is determinable from the declaration of the type, so it doesn't require looking into bodies to figure out - ignoring Chapter 13 effects of course, which are usually erroneous if they have this sort of effect). And I'm assuming that function side-effects are declared somehow. (Without these things, you can't do any call optimizations without either looking in bodies or appealing to the Pure permissions of 10.2.1 - which are rarely applicable.) I agree that Ada 2012 doesn't go far enough to define these things. The global in/global out contracts that we worked on but ended up abandoning as insufficiently fully baked certainly would have helped a lot. We actually tried to come up with a rule for 11.4.2 that would have allowed such optimizations in all cases (that is certainly the intent -- that "assertions" that contain any sort of side-effects are bad). We didn't put it into the Standard because we weren't able to draft one that didn't throw out good things with the bad. But the intent is still there, and it's possible that such a rule (a version 10.2.1(18) for 11.4.2) will appear in the future. >So, in summary, optimizing out predicates in pre- and postconditions may >not be that easy. That's probably true in Ada 2012, especially if you don't use implementation-defined stuff like Pure_Function (in GNAT). That's why I was babbling about an Ada-like language with an extension to constraints that could carry the missing information. Perhaps there is a way to get that information into Ada as well (I'm not as sure). Randy.