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!Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Tue, 23 Dec 2014 17:02:43 -0600 Newsgroups: comp.lang.ada Date: Tue, 23 Dec 2014 18:02:42 -0500 From: Peter Chapin X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu Subject: Re: {Pre,Post}conditions and side effects In-Reply-To: <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> User-Agent: Alpine 2.11 (CYG 23 2013-08-11) Organization: Vermont Technical College MIME-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="3735943886-180244447-1419375764=:4196" X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-nd70BwHXKzTXtjo6LZc6louPnT9rB/tiwLzR7i5uZcsDrCcWca7xR/P0dcVtDZox/l+W6dBV0NFua0C!O7xlxJtv1z7dl4prTfCYiNYiqSOJoArHAL2rCBOyBSb9TBw7nTQhdMw6KUkmqcdCLc/38nDUcsex!k9k9OTMZEqISWd0StA== X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 3653 Xref: news.eternal-september.org comp.lang.ada:24212 Date: 2014-12-23T18:02:42-05:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --3735943886-180244447-1419375764=:4196 Content-Type: TEXT/PLAIN; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Tue, 23 Dec 2014, Jean Fran=E7ois Martinez wrote: > Most of the time you don't write pre/postonditions/invariants involving= =20 > (with functions called) tens of thousands of programming lines and=20 > gazillions of CPU cycles I think, actually, it is fairly common for assertions to require=20 "gazillions" of CPU cycles. In fact, it is easy to come up with examples=20 where the pre- and postconditions take far longer to execute than the=20 subprogram to which they are attached. A simple example that I love because it is so simple yet so telling is=20 binary search of an array. A reasonable precondition is that the array it= =20 is given is sorted. It might look like Pre =3D> (for all I in A'First .. A'Last - 1 =3D> (A(I) <=3D A(I + 1))= ) This takes O(n) time to evaluate. Yet binary search is an O(log(n))=20 algorithm. For large arrays the precondition might take many thousands or= =20 even millions of times longer to execute than the subprogram itself. I don't think there is anything particularly unusual about this example.=20 Here's another case: suppose you had a procedure that added an item to=20 some kind of balanced binary tree. The postcondition might assert that the= =20 tree is still balanced in whatever sense is appropriate... probably an=20 O(n) operation. Yet the insertion procedure is probably O(log(n)). It's=20 easy to imagine many examples. For this reason I assume that in most cases programs must be deployed with= =20 assertions disabled or else there is little chance the program will be=20 able to meet its performance goals. Thus putting anything resembling=20 essential program logic in an assertion is, of course, just wrong.=20 Forbidding assertions with side effects might be nice, but the programmer= =20 still has to be careful with them anyway. Peter --3735943886-180244447-1419375764=:4196--