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: Thu, 8 Dec 2016 09:57:32 +0100 Organization: Aioe.org NNTP Server 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: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; 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:32676 Date: 2016-12-08T09:57:32+01:00 List-Id: 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. >> 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 > 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de