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!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Wed, 14 Dec 2016 21:04:51 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> NNTP-Posting-Host: s3c6wwRqkurrfTZpuYYZ+w.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32831 Date: 2016-12-14T21:04:51+01:00 List-Id: On 2016-12-14 20:23, Shark8 wrote: > On Wednesday, December 14, 2016 at 1:42:34 AM UTC-7, Dmitry A. Kazakov wrote: >> On 13/12/2016 23:13, Shark8 wrote: >>> >>> So? >>> The construct "Procedure X( Y: Positive );" has to have Y checked at >>> runtime in the general case. >> >> X is an integer operation, defined on Integer Y. > > And the contract here states that the value of said integer is positive. No it does not. > The [implicit] contract also states (via LTM) what should happen if > this is violated: CONSTRAINT_ERROR. It is explicit, written in the declaration of procedure X, Y : Positive. >> The precondition here is *not* (Y in Positive), it is (Y in Integer). > > You are observably wrong. > If you supply a negative number, the body of X never executes. Of course it does. Semantically any effect of a call to X is due to X's body. There is nothing else there. >> It is legal to call X on any Integer. Checking Y>=0 is semantically a >> part of the X's body, even if the compiler could inline this part at the >> caller's side or optimize it or the rest of the body away. > > Of course you're utterly ignoring a very important fact: > Ada was designed to (a) be implementable, (b) have static checkers > [indeed, a *lot* of static checking is mandated by requirements of the > translator], and (c) be optimizable. -- In fact, DIANA was designed to > facilitate (b) and (c) by providing a "common language" that > static-analyzers, optimizers, and code-generators could all "speak". Naturally I ignore all this as irrelevant to the issue at hand. It is legal to call X with any integer. Period. > In this light, integrating SPARK proving with the Ada compiler could > allow for better optimizations... and if it can be done in such a way > that it can be leveraged in other portions of the compiler (say semantic > checks), then why not use it? When that comes into life, programmers surely will, though not in the form of preconditions, because as I said, it is bad design. The rule is weakening preconditions, strengthening post-conditions. >>> Ok, I'm looking at the original post... it's another post, and on >>> this thread, but doesn't really seem germane to the point you're trying to >>> make. ;) >> >> No need to look further the difference between evaluation of some P(x) >> and proving Q |= P. These are just different things. Georg attempts to >> sell former for the latter. Won't happen. > > Read this -- > https://www.cs.unm.edu/~forrest/publications/negsharingilcp.pdf -- it's > intuitively obvious how this is a possible answer to my original > posting; it's also obvious how it can be used in solvers, since that's > the particular domain the paper's about. I don't see how is it relevant. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de