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!matrix.darkstorm.co.uk!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: On contracts and implementations Date: Fri, 12 Jul 2013 16:30:23 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <51de7c5d$0$6566$9b4e6d93@newsspool3.arcor-online.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1373664624 23574 69.95.181.76 (12 Jul 2013 21:30:24 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 12 Jul 2013 21:30:24 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:16335 Date: 2013-07-12T16:30:23-05:00 List-Id: "Peter C. Chapin" wrote in message news:ieWdnXSAKPXPAEPMRVn_vwA@giganews.com... ... > I think the litmus test for contract code vs "ordinary" code is that the > contracts should be removable without changing the functional behavior of > the program. This means that any checks of errors arising from the > execution environment, such as missing files or bad user input, can't be > in contracts. > > It is important to be able to remove contracts for performance reasons. > I'm not talking about the constant time overhead of extra range checks. > I'm talking about major performance costs. > > For example a binary search function might reasonably have a pre- > condition that states the input array is sorted. Checking that contract > requires O(n) time and is thus asymptotically slower than the function > itself. One might be able to tolerate that during testing on small data > sets. Furthermore it would be useful to be able to prove that nowhere is > the function called with an unsorted array. However, it is unlikely that > the deployed program could tolerate the slow down in asymptotic running > time. On a full sized data set we might be talking about a 1,000,000x > reduction in speed! I understand your point, but I think it's short-sighted to think about removing the contracts. If you do so, then the contracts can't be used to "hoist" what otherwise have to be checks in the code (as in Text_IO, the containers, and many other packages). Turning off these checks in language-defined code is a complete non-starter, the result would not meet the language specifications (and would introduce erroneousness where none currently exists). Secondly, as compiler's proof abilities increase, most of these contract assertions will disappear. The compiler will be able to prove that they always will succeed, and thus no check will be made. After all, this is the case with existing constraints and exclusions. Compilers work overtime to eliminate unnecessary checks, and tend to remove 60-80% of the checks. It's rare that I see an explicit range check when I examine generated code these days. The same should happen to assertion checks (but only if they are well-written, using globals annotations and/or expression functions). To look further at your example, I agree that evaluating Is_Sorted could be prohibitively expensive. But how did that object *get* sorted? One presumes that it was explicitly sorted somewhere, in which case that routine has an Is_Sorted postcondition. If the compiler can tie those together, there certainly is no need to reevaluate the Is_Sorted on a following precondition. Similarly, the compiler may have been able to prove that the Is_Sorted postcondition is always true. In that case, that won't be executed either. So you still will have the safety of checks on, and *still* have no actual overhead. Now, obviously, these things won't always be next to each other; the array might have been a parameter. But in that case you can use a predicate to ensure that that parameter Is_Sorted, pushing the optimization to another level. To summarize, I expect these to become much like range checks. You'll sometimes have to suppress them, but it will be pretty rare, and often you can add some subtypes in appropriate places to remove the checks rather than actually suppressing them (the latter being more dangerous). Randy.