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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham 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.135.231 with SMTP id pv7mr6282142pbb.8.1328325407242; Fri, 03 Feb 2012 19:16:47 -0800 (PST) MIME-Version: 1.0 Path: lh20ni258048pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!newsfeed.x-privat.org!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Fri, 3 Feb 2012 21:16:34 -0600 Organization: Jacob Sparre Andersen Research & Innovation 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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1328325402 26152 69.95.181.76 (4 Feb 2012 03:16:42 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 4 Feb 2012 03:16:42 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-02-03T21:16:34-06:00 List-Id: "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. (Personally, I get confused when people start going beyond basic boolean logic; I'd rather people didn't even bother to go beyond that because it's worthless to the majority of programmers.) 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. 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. 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. And that is exactly what you are arguing -- and it should be clear to any Ada programmer that that is a fallicy. Similarly, describing *part* of the semantics of a subprogram with a postcondition, and part with comments is perfectly valid and possibly useful. (That's especially true as checking many of the requirements might be too expensive at runtime, and thus they practically have to be omitted from the formal postcondition.) Randy.