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: Georg Bauhaus Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Wed, 13 May 2015 08:58: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> <87egml511m.fsf@theworld.com> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Wed, 13 May 2015 06:57:12 +0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="df34ca51750e189861ff7872c28fb0bf"; logging-data="18926"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19LsoUDsq+FoqmWnlLlriWcMxkR+3f7nxY=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 In-Reply-To: Cancel-Lock: sha1:KIbBplL78ZkBCeVPdxvCVXcr8ds= Xref: news.eternal-september.org comp.lang.ada:25859 Date: 2015-05-13T08:58:19+02:00 List-Id: On 13.05.15 00:37, Randy Brukardt wrote: > "Bob Duff" wrote in message > news:87egml511m.fsf@theworld.com... >> "Randy Brukardt" writes: >> >>> I can see that are some cases where the properties are too expensive to >>> verify at runtime. It would be nice if there was a way to turn off those >>> (AND ONLY THOSE) properties. But Ada doesn't have that sort of >>> granularity, >> >> Sure it does. If Is_Sorted is too slow for production use, you can say: >> >> ... with Predicate => (if Slow_Mode then Is_Sorted(...)) >> >> and set the Slow_Mode flag to True for testing. Also set it to True >> when running proof tools. > > Of course. That's essentially what I've ("we've", really, Isaac created a > lot of the tracing stuff in Janus/Ada) been doing for years. I just hadn't > thought of trying to use it directly in the assertions. We'd use a function > call, though, rather than a constant: > > ... with Dynamic_Predicate => (if JTrace.Trace(Current_Unit) then > Is_Sorted(...)) Given this fine-grained run-time configuration (another IF and then a little something like a debugging thing from an implementation), is the condition in the same category of expressions as Is_Sorted? The second, Is_Sorted, is strictly about the parameters, contractual, so to speak. The first looks rather different and distracting to me. But in any case, then, maybe having a way of influencing the selection of checks could be expressed as pragma Assertion_Policy (Post => Check and not MR_Is_Prime'Post); Stipulating that policy_identifier in Assertion_Policy becomes just a little more flexible by turning the conditional into a portable feature specifiable outside the contracts, but near them: pragma Assertion_Policy( assertion_aspect_mark => policy_setting {, assertion_aspect_mark => policy_setting}); policy_setting ::= policy_identifier { and mute_list } mute_list ::= not defining_identifier'matching_mark {, not defining_identifier'matching_mark }