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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.237.62.144 with SMTP id n16mr23021350qtf.60.1481743412067; Wed, 14 Dec 2016 11:23:32 -0800 (PST) X-Received: by 10.157.37.125 with SMTP id j58mr6984825otd.18.1481743412026; Wed, 14 Dec 2016 11:23:32 -0800 (PST) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!p16no494037qta.1!news-out.google.com!u18ni4059ita.0!nntp.google.com!b123no131568itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 14 Dec 2016 11:23:31 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=67.0.242.189; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 67.0.242.189 References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Ada 2012 Constraints (WRT an Ada IR) From: Shark8 Injection-Date: Wed, 14 Dec 2016 19:23:32 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:32827 Date: 2016-12-14T11:23:31-08:00 List-Id: On Wednesday, December 14, 2016 at 1:42:34 AM UTC-7, Dmitry A. Kazakov wrot= e: > 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. >=20 > X is an integer operation, defined on Integer Y. And the contract here states that the value of said integer is positive. The [implicit] contract also states (via LTM) what should happen if this is= violated: CONSTRAINT_ERROR. >=20 > 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. > It is legal to call X on any Integer. Checking Y>=3D0 is semantically a > part of the X's body, even if the compiler could inline this part at the= =20 > 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) a= nd (c) by providing a "common language" that static-analyzers, optimizers, = and code-generators could all "speak". Many of the static checks that Ada demands of the translators were, at the = time (Ada 83), bleeding-edge technology. SPARK is a step in that direction = though with static-analysis and proof-checking rather than optimization -- = but proof-checking allows many more opportunities for optimization, and may= be said to be the basis of optimization (if you can prove construct X is b= etter than construct A by some metric, and both are equivalent, you can opt= imize for that metric by replacing all occurrences of A with X). 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? > > 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 tryin= g to > > make. ;) >=20 > No need to look further the difference between evaluation of some P(x)=20 > and proving Q |=3D P. These are just different things. Georg attempts to= =20 > sell former for the latter. Won't happen. Read this -- https://www.cs.unm.edu/~forrest/publications/negsharingilcp.pd= f -- 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.