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!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Intervention needed? Date: Mon, 1 Apr 2019 16:42:16 -0500 Organization: JSA Research & Innovation Message-ID: References: <6e1977a5-701e-4b4f-a937-a1b89d9127f0@googlegroups.com> <6f9ea847-2903-48c8-9afc-930201f2765a@googlegroups.com> <87a7hgvxnx.fsf@nightsong.com> <4e240c66-dce8-417f-9147-a53973681e29@googlegroups.com> <28b6a472-6c3a-40a6-8a96-2e27a65ab2ef@googlegroups.com> Injection-Date: Mon, 1 Apr 2019 21:42:16 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="25328"; mail-complaints-to="news@jacob-sparre.dk" 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.7246 Xref: reader01.eternal-september.org comp.lang.ada:56039 Date: 2019-04-01T16:42:16-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:q7tfi3$1483$1@gioia.aioe.org... > On 2019-04-01 17:13, Optikos wrote: > >> One clarifying question that I have is: how would you "prove no >> Constraint_Error propagating"? At run-time or at compile-time or at >> engineering-time using tools other than the compiler? > > It must be the compiler. The programmer states contracts of the > subprograms and if the contracts cannot be proven to hold that is a > compile-time error. > > The problem is, of course, specifying the mandatory strength of a proof > AKA false negatives vs. false positives. If a fact cannot be proven true > by one compiler that makes the program illegal even if another compiler > could prove it. The problem with that is that in the canonical Ada description, it's always possible for a check to fail. One would need to describe in precise terms what "optimizations" of checks that a compiler is mandated to do, or the "proof" would be pointless. That is, in the hypothetical: function Foo return Natural with Exceptions => null is (0); this is illegal in the general case, since this function can raise Constraint_Error (from the conversion of the literal to Natural) and Storage_Error (since everything can raise Storage_Error). One could imagine trying to invent a set of rules of which check optimizations have to be made (a conversion of a literal to a subtype only raises an exception if it actually out of range; a conversion of an object of a subtype to the same subtype never raises an exceptions; and so on), but such a set of rules would either be massive and put a lot of burden on compilers (especially existing compilers), or would be full of holes and thus little could be written this way. My preference for this check is to make it implementation-defined (possibly with a few minimum requirements). Thus, one compiler might be able to compile Foo and another would not -- but it would reflect reality. A compiler that is smarter about checks would be able to handle more code, all the way up to the level of SPARK (where most code could be proved to not raise exceptions). For Janus/Ada, I'm working toward having (optional) warnings for the raise of any exception; that, combined with warnings-as-error mode can give the effect of preventing any exceptions other than ones explicitly expected. It's pretty much all that can be done within Ada as it stands. But that is not as good as an exception contract (especially as exceptions that you want to raise become a pain). Randy.