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 10mr8263675pbf.2.1322145103256; Thu, 24 Nov 2011 06:31:43 -0800 (PST) Path: lh20ni13024pbb.0!nntp.google.com!news2.google.com!news3.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 24 Nov 2011 15:31:27 +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> <1cjufyo57vlpg$.11kf45cs5vnb7.dlg@40tude.net> <4ece213a$0$6629$9b4e6d93@newsspool2.arcor-online.net> <8x9yu4nouq37.16b919ashpomb$.dlg@40tude.net> In-Reply-To: <8x9yu4nouq37.16b919ashpomb$.dlg@40tude.net> Message-ID: <4ece5540$0$6584$9b4e6d93@newsspool3.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 24 Nov 2011 15:31:28 CET NNTP-Posting-Host: c41dc782.newsspool3.arcor-online.net X-Trace: DXC=g[39co`JK^7i6K;>iZ]763McF=Q^Z^V384Fo<]lROoR18kF:Lh>_cHTX3j=]V9_SiL7X17 X-Complaints-To: usenet-abuse@arcor.de Xref: news2.google.com comp.lang.ada:14603 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2011-11-24T15:31:28+01:00 List-Id: On 24.11.11 14:14, Dmitry A. Kazakov wrote: > There is no such thing as assumption, there are only conditions for > whatever outcome of which, the program's behavior must be defined. When I state a condition and have no proof that the condition is correct WRT such-and-such, then my statement is based on assumptions. Let's be honest. BTW, assuming looks like a normal mathematical gesture to me: "Assuming that P(x, y) is true, we show that Q(x, y, z) is true." Why do mathematicians do this if their work hinges on statically unproven P(x, y)? >> Like when showing that for a stack object, the sequence >> (not Is_Full, Push, Pop) is a safe sequence, > > It is not safe: I didn't say that it is safe. I said it is (a) safe sequence, ceteris paribus (listing these) and (b) safe sequence because, to quote you, "The contract might imply behavior (safety of this sequence under certain conditions), when provable." The sequence of operations (not Is_Full, Push, Pop) is provably o.K. by the contract shown because of a 1:1 correspondence of the type's invariant (ensuring capacity and not Is_Full), the postconditions and preconditions at each step. Therefore, checks will be redundant. > 2. immutable stack has one Is_Full. If by immutable you mean a constant view, what's the point? If by immutable you mean a discriminant won't change, Is_Full may still not be constant function. I guess I don't understand. > It is also pointless to use undecidable propositions for static proofs > (which is basically the idea behind dynamic checks). Garbage in, garbage > out. Yes. If I knew SPARK better, I might say something about proof functions, but I don't.