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.1 required=5.0 tests=BAYES_00, PP_MIME_FAKE_ASCII_TEXT autolearn=no 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!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Mon, 22 Dec 2014 17:32:21 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1419291142 5647 24.196.82.226 (22 Dec 2014 23:32:22 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Mon, 22 Dec 2014 23:32:22 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:24200 Date: 2014-12-22T17:32:21-06:00 List-Id: "Jean François Martinez" wrote in message news:2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com... >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. This was proposed with the original proposal. It was eventually dropped because it is too hard to define what a side-effect actually is (easy definitions are too fierce). We tried to invent a "Global" aspect for Ada 2012, but it was considered too complex and too immature for Ada 2012. We're going to try again (with the parallel effort) for the next version of Ada. Second, we did insert a rule which gives an implementation permission to reject assertions with result-changing side-effects. (11.4.2(27/3)). One hopes that as compiler technology improves, implementations will take some advantage of this to reject uses that clearly cause trouble. Third, we also introduced expression functions so that the compiler can see more (or all) of the parts of an assertion. We hoped that would allow more static analysis (including rejection of bad side-effects). To summarize, we spent a lot of time agonizing about this particular issue, wording solutions, and the like. It's most certainly not the case that it wasn't considered, but more that we felt that the alternative of strong restrictions would be barely usable. Randy Brukardt, ARG Editor.