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 Received: by 10.68.36.6 with SMTP id m6mr6312968pbj.4.1322099162929; Wed, 23 Nov 2011 17:46:02 -0800 (PST) Path: lh20ni11057pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!news.internetdienste.de!noris.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 24 Nov 2011 02:36:47 +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> <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> <12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net> <4ecc35b8$0$7628$9b4e6d93@newsspool1.arcor-online.net> <4eccd5d2$0$6637$9b4e6d93@newsspool2.arcor-online.net> <14p8llstxrtci$.18hb93fkpteuv$.dlg@40tude.net> <4ecd0652$0$6582$9b4e6d93@newsspool3.arcor-online.net> <1wyybnjde2yxq.1w37r5182t0xt.dlg@40tude.net> In-Reply-To: <1wyybnjde2yxq.1w37r5182t0xt.dlg@40tude.net> Message-ID: <4ecd9faf$0$6627$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 24 Nov 2011 02:36:47 CET NNTP-Posting-Host: 15b800bb.newsspool2.arcor-online.net X-Trace: DXC=aBaT@1^`>Lf]l@YUW5NBknA9EHlD;3Ycb4Fo<]lROoRa8kFejVhlBkIO^noWbcKNh8;oER_Mo X-Complaints-To: usenet-abuse@arcor.de Xref: news2.google.com comp.lang.ada:14584 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Date: 2011-11-24T02:36:47+01:00 List-Id: On 23.11.11 20:48, Dmitry A. Kazakov wrote: >>>> Subprograms of unknown effect, >>> >>> You confuse interface and implementation. >> >> I call a subprogram because it has an effect. Is this unusual? >> In order to choose the right subprogram, I need to know its >> effect. > > That is exactly why contracts cannot be dynamic. Dynamic means statically > undecidable. How are you going to know anything about the subprogram, if > that is unknown until run-time? The typical example is a stack and its contract referring to values available at runtime: from the contract, I learn that a stack is initially empty and has a certain capacity. When there is room (which is the case after object creation), I may push an element on top of the stack. From the postcondition of `push`, I learn that the stack is not empty after the execution of `push`. Not being empty is the precondition of `pop`. Hence, the sequence create push pop is safe in whichever implementation, provided the programmers follow the contractual obligations. Similarly, for Sqrt, Ada throws Argument_Error if the caller fails to establish the implicit precondition of Sqrt: that the argument must be an element of the domain of the corresponding mathematical function. In this case, one might specify pre => (X >= 0.0) where X is of type Float_Type'Base, Float_Type being the generic formal. I could learn something about the result of Sqrt from its postcondition. Sometimes the postcondition can use simpler functions to express the result that a programmer should expect. But while Sqrt'Result * Sqrt'Result = X does not work (because computers will not compute mathematical results in many cases), expressing the other part of Sqrt's postcondition (LRM A.5.1(12)) is possible: post => (Sqrt'Result >= 0.0) There are implementation requirements, too, so post => (if X = 0.0 then Sqrt'Result = 0.0 elsif X = 1.0 then Sqrt'Result = 1.0 else Sqrt'Result >= 0.0) Is Sqrt'Result statically determinable? Statically useful? I guess there is information in the postcondition that can be used during development and also by source text analysis. Should the postcondition give a maximal result in terms of attributes of Float_Type'Base? But certainly, if some Sqrt purports to implement the contract and then a runtime check of the postcondition raises an exception, this is an effect caused by not following the contract. If the postcondition is correct, fix the implementation, then. > One nice thing about inconsistencies is that they corrupt the whole system > of reasoning. You cannot presume "for practical reason" that 2+2=5, because > that will ruin everything else. Ruin depends on the frame of reference. There is good reason to frown at first vis-�-vis the fact that 99 / 100 = 0. A language design first needs to establish the rules by which 99 / 100 = 0. Only then one may study programs and say which things make sense and which ones do not. Meyer's frames of reference transcend the logic of just programs in several dimensions, I think. For illustration, he contrasts obligations moving work between client and supplier and identifies styles of DbC: if a subprogram is lenient and accepts everything, it tends to deal with all cases. If a subprogram is demanding, then only suitable values can be supplied and the implementation is simpler, having lead to simpler systems. One may try either style in some larger project and observe the outcome. >>>>>> There is no right or wrong in most programs. >>>>> >>>>> You cannot build safe software on false premises. >>>> >>>> Almost all programs have a number of things that can go wrong, >>> >>> Program code cannot GO wrong, it IS either wrong or not, here and now. >> >> No, we don't know whether an executable program is right or wrong, >> for almost all programs. > > It is not about anybody's knowledge. A program is correct or not > independently on whether you or anybody else knows that. "Is correct or not correct" sounds like a tautology and says just as much. For any k in a numbering of programs P, all we can say is that P(k) may be correct or not. We cannot say "P(k) is correct" before studying P(k) and we also cannot say "P(k) is not correct" before studying P(k). Informally speaking, then, things can go wrong, because we know only that the program is correct or not.