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: border1.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!1.eu.feeder.erje.net!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: Wed, 13 May 2015 20:21:39 -0500 Organization: Jacob Sparre Andersen Research & Innovation 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> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431566500 26433 24.196.82.226 (14 May 2015 01:21:40 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 14 May 2015 01:21:40 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: number.nntp.giganews.com comp.lang.ada:193178 Date: 2015-05-13T20:21:39-05:00 List-Id: "Georg Bauhaus" wrote in message news:miusk8$ife$1@dont-email.me... > 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. I think I made that point in my original message; this looks rather heavy and hurts the readability of the predicates. But that certainly could be reduced by naming and defaults. -- At the start of the package: Check : renames JTrace.Trace(Current_Unit); ... with Dynamic_Predicate => (if Check then Is_Sorted(...)) That certainly depends upon your needs; I typical use 3 or 4 levels of tracing crosscut with subsystem or package level control. That might be overkill for many, and perhaps Bob's direct solution would be enough for you. Randy.