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=ham 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!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!news.karotte.org!news.musoftware.de!wum.musoftware.de!news.tornevall.net!news.jacob-sparre.dk!pnx.dk!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: MI is sloppy Date: Fri, 12 Dec 2008 18:08:12 -0600 Organization: Jacob Sparre Andersen Message-ID: 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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1229126923 24983 69.95.181.76 (13 Dec 2008 00:08:43 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 13 Dec 2008 00:08:43 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5512 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 Xref: g2news1.google.com comp.lang.ada:2981 Date: 2008-12-12T18:08:12-06:00 List-Id: "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). 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. What a programming language can't do is mandate the cases in which that detection will occur. 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.) ... >> 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). ... >> If we wanted more of the minor differences covered >> by type hierarchies, we might end up with a Qi type >> system... For Ada? > > 1. Qt is not a programming language. > > 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. > 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. Randy.