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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC 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!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Tue, 09 Jun 2015 14:02:19 +0200 Organization: A noiseless patient Spider Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <87oali5i6n.fsf@adaheads.sparre-andersen.dk> <87617povr4.fsf@adaheads.sparre-andersen.dk> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Tue, 9 Jun 2015 12:01:05 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="b96887e80893c84a90c3007226ca0d1c"; logging-data="30056"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18gnuGkEdN4G7V9XzYgKJyO4/HGsfnnHn4=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:31.0) Gecko/20100101 Thunderbird/31.7.0 In-Reply-To: Cancel-Lock: sha1:xou6Pu8SU90DSjLPUk+i9QfxXaM= Xref: news.eternal-september.org comp.lang.ada:26236 Date: 2015-06-09T14:02:19+02:00 List-Id: On 09.06.15 09:55, Stefan.Lucks@uni-weimar.de wrote: > On Tue, 19 May 2015, Jacob Sparre Andersen wrote: > >> Stefan.Lucks@uni-weimar.de writes: >>> >>> (for all I in 2 .. N-1 => (N mod I) /= 0) >>> >> I don't need a profiler to estimate that it takes long time to execute, >> but I need a profiler to see where the compiler can't eliminate it from >> a critical path through static analysis. > > Sorry, i forgot about this thread ... so my response is somewhat late. > > If N is large enough, the compiler would have to eliminate that > expression from all paths, not just from its critical path. (Think of N > \approx 2**60. Which comes first: your program passing or failing all > test cases, or your retirement?) > >> Good. I noticed an interesting proposal for an extension to the >> assertion policy control in one of the posts in this thread. I suppose >> we should push to have the ARG accept this (or something similar). > > Agreed! It has been suggested in some places that assertion control should be exercised with the help of a Config package. with $Condition$ => (if Config.Is_Expensive_Test_666 (N) then True else (for all I in 2 .. N-1 => (N mod I) /= 0)); While it was considered practical, maybe even charming because Config is just Ada, allowing to choose configuration names, permitting conditional conditions (cf. N above), it would inevitably introduce idiosyncrasies and, more importantly IMO, shift attention to Config stuff. The latter could be considered off-topic the more it reflects a project's own vocabulary, which cannot be as universally familiar as a quantified_expression. Does Config belong in a contract? Moreover, aspects that allow one to address the issue at the language level, outside the contract, not using mere conventions, would be more standard, and meet standard expectations. Somewhat like contracts always define things and state when a thing does apply, and to what. These aspects and the notion of configuration do not need to exclude each other, if the words Configuration Pragma imply that.