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!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!fx09.iad.POSTED!not-for-mail From: Brad Moore User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.3.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> In-Reply-To: Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 8bit Message-ID: NNTP-Posting-Host: 68.145.219.148 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: 1419278372 68.145.219.148 (Mon, 22 Dec 2014 19:59:32 UTC) NNTP-Posting-Date: Mon, 22 Dec 2014 19:59:32 UTC Date: Mon, 22 Dec 2014 12:59:31 -0700 X-Received-Bytes: 3599 X-Received-Body-CRC: 1680382887 Xref: news.eternal-september.org comp.lang.ada:24197 Date: 2014-12-22T12:59:31-07:00 List-Id: On 14-12-22 12:38 PM, sbelmont700@gmail.com wrote: > On Monday, December 22, 2014 11:22:29 AM UTC-5, Jean François Martinez wrote: >> Perhaps it would have been a good idea to have a No_Side_Effects aspect and only functions labelled with this pragma would be allowed in pre/post conditions. Such functions would not be able to modify global variables and would be restricted to invoking only functions/procedures marked with this aspect. This is somewhat akin with the restrictions for packages marked with elaboration pragmas or with pragmas realated to distributed system annex. In both a package may only with a "lower or equal" package. >> > > It's more than just global variables, though. Your condition might be thusly ludicrous: > > function P return Boolean is > x : Some_Ptr_Type := new Integer'(42); > begin > return True; > exception > when others => Some_Task.Blocking_Rendezous; > end P; > > Now you've got a function that doesn't access any global variables, but not only randomly exhaust the heap, but also permanently blocks the thread, so you are right back where you started. You end up needing all the same rules and restrictions as pragma Pure, which means you might as well just be beholden to pragma Pure to begin with (or use qualified expressions). The value designated by X is a global variable though. In the proposal for the Global aspect which appeared in a paper at the most recent HILT conference, you would not be allowed to specify function P return Boolean with Global => null; for this case, as the value designated by Some_Ptr_Type actually is a global variable. You could however write; function P return Boolean with Global => (in out => Some_Ptr_Type); However, this function now obviously has side effects > > But more to the point, there is no escaping that disabling/enabling checks will cause the program to function differently; that is, after all, the entire point. What constitutes 'correctness' is only in the eyes of the programmer. Ergo: > > procedure Some_Subprogram is null with Pre => false; > > procedure Insane is > begin > Some_Subprogram; > raise Program_Error; > exception > when others => Continue_Running; > end Insane; > > No globals, but it still "breaks" when checks are disabled. I don't see anything being broken here. Some_Program still honours it's contract, and does what it says it will do. The contract of Some_Program doesn't impact the Insane procedure's contract. You haven't shown any contract for Insane, so for all we know, it has no contract, and do anything, including what you have here. Brad > > -sb >