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!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Fri, 9 Dec 2016 15:46:53 -0600 Organization: JSA Research & Innovation Message-ID: References: <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1481320014 18803 24.196.82.226 (9 Dec 2016 21:46:54 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 9 Dec 2016 21:46:54 +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: news.eternal-september.org comp.lang.ada:32703 Date: 2016-12-09T15:46:53-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:o2b79r$1dit$1@gioia.aioe.org... > On 07/12/2016 23:26, Randy Brukardt wrote: >> "Dmitry A. Kazakov" wrote in message >> news:o28non$1fn8$1@gioia.aioe.org... >>> On 07/12/2016 00:15, Randy Brukardt wrote: >> ... >>>> Moreover, most contracts (at least the ones I'd write) raise specific >>>> exceptions (not Assertion_Error). Indeed, this is a far better way to >>>> define >>>> something that raises an exception than an English comment. (Which is >>>> the >>>> only other alternative for the specification - and its the >>>> specification >>>> that matters, not the body.) >>> >>> As I said in another post it is a bad idea. The list exceptions, their >>> names, must tell the reader when they are to propagate. You could >>> specify >>> the exact condition in a few very limited cases. In a real life scenario >>> you cannot specify the Boolean expression guarding Disk_Error. Moreover, >>> in most cases that would be an over-specification. >> >> I never meant the above to be exclusive. Sometimes, as you say, an >> exception >> is raised by something external to the Ada program, and that is probably >> besst described in English. I was just talking about exceptions that >> depend >> only on the parameter values. > > That does not change much. In most cases you still cannot do that without > having the expression as complex as the body itself. Instead of one > implementation you have two and thus you double the opportunity for making > an error. One surely hopes that you aren't repeating the preconditions in the body. That's madness. >>> My point is that either you don't need the expression or else it >>> must/can >>> be statically provable and thus become a proper pre-/post-condition with >>> no exceptions involved. >> >> Not everything can be statically proven (think Unchecked_Conversion), and >> a >> lot of stuff can only be proven in a full-program scenario, so I'm >> dubious >> of the above in any case. But even if that turns out to be possible years >> from now, I'm more interested in what I can do today -- especially if it >> is >> likely to be helpful to present (i.e. Codepeer) and future provers. > > Right > >> A >> dynamic check that can be proven (or better proven and eliminated by the tested-------------------------^^^^^ >> compiler) helps more than specifications with no machine-processable >> description. > > Wrong. The proper way to do this is elevate the check into the behavior > and contract an exception. Later, when proofs are mature, client could > prove absence of the exception. Nothing lost, everybody is happy. That's precisely what Ada 2012 contracts do. You can't leave this sort of behavior hidden to clients, or mixed in with the rest of the body (unless you have abandoned the idea of separation of specification [what the caller needs to know] and body [what the caller does *not* need to know]). Randy.