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,ad06d2d7cb045687 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.73.229 with SMTP id o5mr6916262pbv.7.1328352493989; Sat, 04 Feb 2012 02:48:13 -0800 (PST) Path: lh20ni259192pbb.0!nntp.google.com!news2.google.com!eweka.nl!lightspeed.eweka.nl!194.134.4.91.MISMATCH!news2.euro.net!feeds.phibee-telecom.net!de-l.enfer-du-nord.net!feeder2.enfer-du-nord.net!gegeweb.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Sat, 4 Feb 2012 11:47:46 +0100 Organization: cbb software GmbH Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> <1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: uPp0VmqFNQ7upgD/pR45FA.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 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-02-04T11:47:46+01:00 List-Id: On Fri, 3 Feb 2012 21:16:34 -0600, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net... > ... >> You and Randy confuse a generalized semantics with an undefined one. The >> key question is the relation of the variance of the generalized/unspecified >> part to the program's behavior. In your example odd values like 1,3 are not >> used by the program, or at least supposed to be unused. In the OP example, >> Format_Error of unspecified semantics is to be used heavily. > > In practice, they're the same thing. It will never be practical to fully > describe the semantics a real program (like, say, an Ada compiler). Even if > someone invents a far more descriptive formalism than plain Ada expressions > to describe such things, it's going to be far too complex to use. Sure, but this is a fault of your (read: ARG) approach. Look, you are trying to describe the semantics of a program written in the language (Ada expression) in the same language (Ada expression), though in the form of "pre-"/"post-" conditions. That would not work. No need to even try! Isn't it obvious, that there is no value added? It is the same language of same power. Why do you expect it work any better by merely moving code from bodies to the declarations? > Beyond that, there is not such thing as "I don't intend to use something". > Unless the program somehow prevents it, *it* will get used and will happen. Absolutely. But that does not imply that a dynamic check could magically make unusable usable. > You will get odd values in the data type that J-P described -- it does not > matter how they happened. And you will be happy (or at least ought to be) > that some bugs are detected even if not all. No, I am very unhappy when the original appearance of a bug is modified by some middleman (e.g. exception propagation). That is assuming absence of false positives. But as we learned from the history accessibility checks, false positives are very likely to happen. When highly qualified Ada designers failed to design a check properly, what to expect from a layman programmer adding fancy pre-/postconditions in his program? > But to claim that just because it's practically impossible to describe the > complete behavior of real systems does not mean that there is no benefit to > describing the easy part. No, if that description is incomplete; No, if that is a dynamic check, rather than a description; No, if the remaining part cannot be implemented because of the choice made; No, if the easy part is unimportant to the goal at hand. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de