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!fx23.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: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> 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: 1419268704 68.145.219.148 (Mon, 22 Dec 2014 17:18:24 UTC) NNTP-Posting-Date: Mon, 22 Dec 2014 17:18:24 UTC Date: Mon, 22 Dec 2014 10:18:19 -0700 X-Received-Bytes: 2932 X-Received-Body-CRC: 4096972952 Xref: news.eternal-september.org comp.lang.ada:24194 Date: 2014-12-22T10:18:19-07:00 List-Id: On 14-12-22 09:22 AM, Jean François Martinez wrote: > First time I read about Pre-Post conditions in Ada 2012 I felt some disconfort about functions invoked in pre/post conditions being allowed to have side effects. Tus it is possible to have programs that work when checks are enabled and break when they are disabled that because the side effets "make them work". I don't like "solutions" like "the compiler will allow you to soot yourself in the foot so be careful". That is C not Ada > > 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. There is a proposal to have a Global aspect to be considered for Ada 202x, that could be applied to subprograms. Such an aspect would indicate if a subprogram body referenced any global variables. It would also indicate if a subprogram references no globals. eg. function Foo (X : Integer) return Integer with Globals => null; I believe such a subprogram would not have side-effects > > First problem I see is that I/O functions have side effect so when debugging No_Side_Effects_functions it would impossible to use the good-old method of inseting Puts in the code. Agreed. I suppose you could comment out the Globals => null during debugging, and uncomment it once the debugging had been removed. > > SEcond and biggest problem is that it is too late. Too late for Ada 2012, but not for Ada 202X. Or you could consider using SPARK 2014 for this code, as it already has this Global aspect. Or you might ask your compiler vender to provide an implementation specific solution. Brad > > Jean François Martinez >