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,ea5071f634c2ea8b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.35.68 with SMTP id f4mr467945pbj.5.1321989333778; Tue, 22 Nov 2011 11:15:33 -0800 (PST) Path: lh20ni6311pbb.0!nntp.google.com!news1.google.com!news.glorb.com!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. Date: Tue, 22 Nov 2011 20:15:33 +0100 Organization: cbb software GmbH Message-ID: <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <4295dc09-43de-4557-a095-fc108359f27f@y42g2000yqh.googlegroups.com> <3snehoqgs8ia$.1nobjem6g6hx6$.dlg@40tude.net> <128rdz2581345$.c4td19l7qp9z$.dlg@40tude.net> <16ipwvpdavifr$.17bxf7if7f6kh$.dlg@40tude.net> <4ecb78b1$0$6643$9b4e6d93@newsspool2.arcor-online.net> <1iofgbqznsviu$.phvidtvxlyj4$.dlg@40tude.net> <4ecbb96e$0$6581$9b4e6d93@newsspool3.arcor-online.net> <4ecbdfdb$0$6629$9b4e6d93@newsspool2.arcor-online.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: ARmOcGB+2dBIwZUEYVS5Gg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news1.google.com comp.lang.ada:19039 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2011-11-22T20:15:33+01:00 List-Id: On Tue, 22 Nov 2011 18:46:02 +0100, Georg Bauhaus wrote: > On 22.11.11 17:23, Dmitry A. Kazakov wrote: > >>> Not sure, are you speaking about DbC (TM)? >> >> I don't care about trade marks and definitions given by reference >> manuals... > > Frankly, doing so in some way will help discussing things. Any discussion should be based on the meaning of words. Discussions about words are uninteresting to me. >>> (b) A debugging ("design", "specification", bla-bla) aid leading >>> towards formally proven components where such proofs are possible. >> >> I cannot decipher this, sorry. > > Meyer: "Programming is a human activity". > Programmers are led towards a solution during the process of programming. > Depending on the characteristics of the process, then, > programmers will produce different results. I see no word "debugging" there. > DbC (TM), as a characteristic of a process, leads to products > that lend themselves to proving them correct more than others, > provided this is possible. I suppose drinking coffee does that as well. CDD [caffeine driven design] (TM). As for randomly raised exceptions from dynamic checks, I doubt that leads to better products. I my experience at least 40% of my debugging efforts in Ada 95 was spent on catching accessibility checks faults. Ada 2005 improved that greatly. To me this is a vivid example why dynamic checks are evil. >>> "An exception is the element's inability to fulfil its contract, for any >>> reason: a hardware failure has occurred, a called routine has failed, a >>> software bug makes it impossible to satisfy the contract." >> >> An exception is a program state. It is not an inability. The behavior in an >> exceptional state is contracted, at least in Ada it is. > > OK, erroneous execution. If the program has a bug its execution is erroneous. Is it what you want to say? So? >>> Without those dynamic checks, we wouldn't ever notice a failure? >> >> How would you notice a failure to notice? > > Really does not matter. There is no need to require forall-qualification > of every aspect of DbC(TM) when it is not meant to be in a program > if and only if the program (including hardware) is proven to be > 100% such-and-such. Impractical. Which then? You have to specify the failures you are going to notice. Once you do qualify them, you would easily be able to avoid them. Note that all the buzz is about noticing something unanticipated. That is impossible, period. Anticipated failures are not bugs, they are states. >> The software which behavior is unknown shall never be executed. > > But this is impossible, in general! I see the point, since it is impossible do right, you are going to do it wrong. I am not arguing for or against your or Meyer's motivations. I only state that it is wrong. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de