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.15.41 with SMTP id u9mr8573594pbc.3.1322152347903; Thu, 24 Nov 2011 08:32:27 -0800 (PST) Path: lh20ni13331pbb.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!gegeweb.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Generic-Package Elaboration Question / Possible GNAT Bug. Date: Thu, 24 Nov 2011 17:32:05 +0100 Organization: cbb software GmbH Message-ID: <9bsjjzx6jp6y$.1ofpm9z0f5ja5$.dlg@40tude.net> 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> <4ece5540$0$6584$9b4e6d93@newsspool3.arcor-online.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.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:19119 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2011-11-24T17:32:05+01:00 List-Id: On Thu, 24 Nov 2011 15:31:27 +0100, Georg Bauhaus wrote: > 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. No, "if A then B" is not based on an assumption of A. B is (in this context). > 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)? Because the mathematician usually stops at P|=Q. In programming you are interested in both P|=... and ^P|=..., so long P is not proven. >>> 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. OK >> 2. immutable stack has one Is_Full. > > If by immutable you mean a constant view, what's the point? That the proposition does not hold for all instances of stack. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de