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!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.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: Wed, 7 Dec 2016 16:26:25 -0600 Organization: JSA Research & Innovation Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <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 1481149581 32505 24.196.82.226 (7 Dec 2016 22:26:21 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 7 Dec 2016 22:26:21 +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:32664 Date: 2016-12-07T16:26:25-06:00 List-Id: "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. > 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. A dynamic check that can be proven (or better proven and eliminated by the compiler) helps more than specifications with no machine-processable description. Randy.