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!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!feed.news.qwest.net!mpls-nntp-02.inet.qwest.net!132.250.1.121.MISMATCH!ra.nrl.navy.mil!bloom-beacon.mit.edu!bloom-beacon.mit.edu!newsswitch.lcs.mit.edu!nntp.TheWorld.com!.POSTED!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Tue, 23 Dec 2014 20:03:37 -0500 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: pcls7.std.com 1419383019 4510 192.74.137.71 (24 Dec 2014 01:03:39 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Wed, 24 Dec 2014 01:03:39 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:iuFCl5lxLlLIXULkF/eySROamUI= Xref: news.eternal-september.org comp.lang.ada:24215 Date: 2014-12-23T20:03:37-05:00 List-Id: Peter Chapin writes: > I think, actually, it is fairly common for assertions to require > "gazillions" of CPU cycles. In fact, it is easy to come up with examples > where the pre- and postconditions take far longer to execute than the > subprogram to which they are attached. > > A simple example that I love because it is so simple yet so telling is > binary search of an array. A reasonable precondition is that the array > it is given is sorted. It might look like > > Pre => (for all I in A'First .. A'Last - 1 => (A(I) <= A(I + 1))) > > This takes O(n) time to evaluate. Yet binary search is an O(log(n)) > algorithm. For large arrays the precondition might take many thousands > or even millions of times longer to execute than the subprogram itself. > > I don't think there is anything particularly unusual about this > example. Here's another case: suppose you had a procedure that added an > item to some kind of balanced binary tree. The postcondition might > assert that the tree is still balanced in whatever sense is > appropriate... probably an O(n) operation. Yet the insertion procedure > is probably O(log(n)). It's easy to imagine many examples. Yes, all that's true. But those would be better as predicates/invariants instead of preconditions. For ex., if you know Sort produces a sorted array, and Binary_Search takes a sorted array, you don't have to check for sorted-ness on entry to Binary_Search if you've got a Sorted_Array. But note that your "Pre" above is a good example of what I was saying in a somewhat-unrelated post in this thread: It is shorter and simpler than doing a sort using some efficient sorting algorithm. > For this reason I assume that in most cases programs must be deployed > with assertions disabled or else there is little chance the program will > be able to meet its performance goals. Yes, or at least SOME assertions disabled. I like to say, "If you don't need to disable assertions, then you don't have enough assertions". It's a silly sound bite that is not always true, but there's a grain of truth in it. >... Thus putting anything resembling > essential program logic in an assertion is, of course, just > wrong. Yes. >... Forbidding assertions with side effects might be nice, but the > programmer still has to be careful with them anyway. Yes. -- Bob