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!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: Tue, 12 May 2015 17:37:49 -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 1431470269 30872 24.196.82.226 (12 May 2015 22:37:49 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 12 May 2015 22:37:49 +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:25856 Date: 2015-05-12T17:37:49-05:00 List-Id: "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(...)) When compiled for testing, JTrace.Trace is a function call which returns true or false based on the selections from a tracing menu that pops up when the tracing options are used. When compiled for production use, Trace is an array with all of the elements set to False. (At least that was the idea, I don't think we ever used it that way.) The downside here is a bit more noise, but the upsides are obvious (Stefan explained them in gory detail). One probably could design something shorter with the same effect (that would cut the noise). Randy. > > Alternatively, you can say something like: > > function Sort(X: My_Array) return My_Array with > Post => (if X'Length <= 20 then Is_Sorted(Sort'Result)); > > Now calls to Sort can be O(log N) instead of O(N). And if Sort doesn't > do anything special for arrays longer than 20, the postcondition is > likely to catch any bugs in Sort. > >> Correct. If it hurts, don't write that. :-) I don't begin to believe that >> all program properties can be proved. > > Yes, that's obviously true. Here's a property of GNAT: > > Compared to most compilers (for any language), GNAT usually gives > better error messages. > > Anybody who has used GNAT and a lot of other compilers knows that > property is true. But nobody can prove it in a mathematical sense, > because there's no way to formalize it. > > - Bob