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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,73f81e5f5d6ee80f X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: MI is sloppy Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <1g29uf1ygl1wc$.1x184o2bk9m0k$.dlg@40tude.net> <1hjx0k7xmfw4n$.14q7chpo1r1ma$.dlg@40tude.net> <49424203$0$31868$9b4e6d93@newsspool3.arcor-online.net> <494255e8$0$31331$9b4e6d93@newsspool4.arcor-online.net> <43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net> Date: Sat, 13 Dec 2008 10:54:10 +0100 Message-ID: <13yddqs9s95ad$.3qs30lg1bvgl.dlg@40tude.net> NNTP-Posting-Date: 13 Dec 2008 10:54:10 CET NNTP-Posting-Host: 02bd2c80.newsspool1.arcor-online.net X-Trace: DXC=dVn[=P2jAiSU6b:FjPaGjQic==]BZ:af^4Fo<]lROoRQ^YC2XCjHcbY?@AV>hR\\>ZDNcfSJ;bb[UIRnRBaCd On Fri, 12 Dec 2008 18:08:12 -0600, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net... >> On Fri, 12 Dec 2008 13:15:35 +0100, Georg Bauhaus wrote: >> >>> Dmitry A. Kazakov schrieb: >>> >>>>> If you have an ambitious compiler, it might reach out, >>>>> at compile time, for objects whose behavior is then known >>>>> to be constrained by membership in a then known specific >>>>> subtype. >>>> >>>> ... and then inline raising Constraint_Error. Great! > > For some reason, I didn't get the other messages to this thread. > > But that's not what I'm suggesting. First of all, this is a contract > failure; it has it's own dedicated exception (maybe Assertion_Error). Does it change anything? > In > addition, I think compilers should be allowed to reject any program in which > that it can be determined statically that the contract exception will > unconditionally be raised. If exceptions where *statically* contracted I would accept assertions (not preconditions) raising them. > What a programming language can't do is mandate > the cases in which that detection will occur. Why? That looks simple: procedure Foo raise Constraint_Error and not Assertion_Error; declare raises not (Constraint_Error or Assertion_Error); begin if False then Foo; end if; end; -- Compile error, the block may propagate -- Constraint_Error, because Foo can The estimation is conservative, it ignores that Foo would eventually never called. > That will depend on the tools > you use; a really good tool should be able to detect just about everything > statically. (In addition, you could use an exception contract to force this, > or the program would also be illegal.) Not an addition (to having nothing), but how things should work, IMO. >>> Deriving another type, even if not sufficiently different >>> from the original to warrant a type, is another formal >>> way to trigger the same effect on the programmer, at compile >>> time: "There is something odd about your program". >> >> No, the effect is fundamentally different. The effect is that the program >> becomes illegal, it may not run. > > That's exactly what is possible with the contracts that I'm suggesting. But > it cannot be mandated; we have to leave to the tools vendors to describe > what is possible to detect statically (after giving them the framework). Leaving legality to vendor tools? Shudder... >> 2. There is no minor differences in terms of correctness. An incorrect >> program is incorrect. > > You are definitely wrong about this, at least in a finite world. The cost to > fix some technically incorrect programs (in manpower, performance, > useability, etc.) is greater than the cost of the error occurring. Such > programs might be technically incorrect, but they're practically correct. > This the reason that we tolerate erroneousness in the language definition. > And it's the reason that we use exception handlers. It is an empiric estimation which nobody can tell how close to reality it is. You can declare any program correct if it will never be started. In order to make such estimations any scientific, you have to enumerate all program states, attach a cost of failure to each one and the probability that the program traverses the state. Basically, what certification process does. Now, because this is technically (and economically) impossible, you usually estimate the program behaviour, based on the assumption that it was implemented more or less correctly. Now the vicious circle is closed. This is a psychotherapy, no more. I don't argue that it does not work. It does. This is why you mailer cannot see all messages in this group... (:-)) >> There is no *any* way to predict the effect of incorrectness. > > That is surely not true. An Ada bounded error occurs in a program that is > incorrect, but the effect of that incorrectness is strictly bounded. No. Bounded error defines the effect for the program execution. It does not define the semantics of. If I wrote I := I + 2 instead of I := I + 1, that would not be an error at all. Yet the program would be incorrect and nobody could tell anything about the effect without knowing what the program does and where it is deployed. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de