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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA 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.0.170 with SMTP id 10mr4808594pbf.2.1322064643154; Wed, 23 Nov 2011 08:10:43 -0800 (PST) Path: lh20ni9556pbb.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!weretis.net!feeder4.news.weretis.net!newsreader4.netcologne.de!news.netcologne.de!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 23 Nov 2011 17:10:41 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:8.0) Gecko/20111105 Thunderbird/8.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. References: <7bf9bc32-850a-40c6-9ae2-5254fe220533@f29g2000yqa.googlegroups.com> <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> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <1ecuhb030iugz.4q1hfjx371xa.dlg@40tude.net> <4ecc393d$0$7625$9b4e6d93@newsspool1.arcor-online.net> <124aq618dmove.884jj64mzm6w$.dlg@40tude.net> <1jxx617mf2cqf$.1j076axdq83mr$.dlg@40tude.net> <4eccd308$0$6623$9b4e6d93@newsspool2.arcor-online.net> <4eccd849$0$6623$9b4e6d93@newsspool2.arcor-online.net> <1n04ab6q3dg0$.1dthih58wz7sl.dlg@40tude.net> <4eccfc43$0$6584$9b4e6d93@newsspool3.arcor-online.net> <1837st224x4qf.1eltyp608r49p$.dlg@40tude.net> In-Reply-To: <1837st224x4qf.1eltyp608r49p$.dlg@40tude.net> Message-ID: <4ecd1b01$0$6552$9b4e6d93@newsspool4.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 23 Nov 2011 17:10:42 CET NNTP-Posting-Host: ea8acfd6.newsspool4.arcor-online.net X-Trace: DXC=R\Pi]An3JJUaAeROF2PWMQ4IUKZLh>_cHTX3j]0j4YZS_97^U X-Complaints-To: usenet-abuse@arcor.de Xref: news1.google.com comp.lang.ada:19091 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2011-11-23T17:10:42+01:00 List-Id: On 23.11.11 15:43, Dmitry A. Kazakov wrote: > On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote: > >> On 23.11.11 14:14, Dmitry A. Kazakov wrote: >>> On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote: >>> >>>> On 23.11.11 12:13, Dmitry A. Kazakov wrote: >>>>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote: >>>>> >>>>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote: >>>>>> >>>>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part >>>>>>> of the implementation? >>>>>> >>>>>> I don't agree. pre/post should specify what the implementation is >>>>>> supposed to do. >>>>> >>>>> In that case they cannot be executable. >>>> >>>> From the point of view of CS trivia, they cannot be executable. >>>> But this point of view is not applicable, >>> >>> I don't see why doing something wrong should make it more applicable. Maybe >>> because the criteria of applicability are distorted as well? Because it leads to self documenting source text that uses this wrong formalism, assertions. >> If it is wrong to assume that a compiler is correct > > It is right that the compiler correctly translates your program. We do not know whether or not a compiler correctly translates a given program unless we show that the translation is correct. If we do, we know that the given run of the compiler on the given program seems to have worked as intended. (ACATS) The only check in a compiler without internal checks is a translation that is checked by humans. A compiler that performs internal checks while it is running may fail and produce a notice of failure. Perhaps it should continue instead and produce a program that shifts a rocket? Is there a compiler out there that is know to work correctly for a set of programs? In this compiler, DbC assertions will be documentation only. > Are you > suggesting to break the compiler because it might be already broken? No.