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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.220.230 with SMTP id pz6mr12453878pbc.3.1341561468748; Fri, 06 Jul 2012 00:57:48 -0700 (PDT) Path: l9ni11017pbj.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Fri, 6 Jul 2012 09:57:50 +0200 Organization: cbb software GmbH Message-ID: References: <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <1i1mp8xs3vtl2.1oc4m66qtfgzq.dlg@40tude.net> <4fe9bde5$0$6566$9b4e6d93@newsspool4.arcor-online.net> <1otknesgpcisl$.112pd12on3vsb$.dlg@40tude.net> <1etm46gu9c54e$.rkbmrzh5ia6$.dlg@40tude.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 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-07-06T09:57:50+02:00 List-Id: On Thu, 5 Jul 2012 23:23:20 -0700 (PDT), Shark8 wrote: > On Thursday, July 5, 2012 1:24:57 AM UTC-6, Dmitry A. Kazakov wrote: >> On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote: >> >>> Also, I don't know where you got the idea that pre- and post-conditions >>> must not implement anything. >> >> Trivial: >> >> IF pre-/post-condition is contract THEN they are not implementation >> [POV #2] >> ELSE ... [POV #1] > > Now you're just restating what you said. No. The propositions are different: P1: The contract may implement [some behavior] P2: Pre-/post-conditions may implement [some behavior] The statement I made was: Pre-/post-condition is contract AND not P1 => not P2 Nobody, so far, take an assault on not P1. Would you? > If you mean something like "I > take that to be axiomaatic" or "by definition [...]" there'd be something > to discuss. Nope. Then, there will nothing to discuss, because a usual trick then, is to refer to the RM claiming that anything you said is irrelevant to Ada. Instead I offered a bait: two options to choose #1 and #2. These two are complete and independent. It cannot be both, it cannot be none. > pre- and post-conditions most of the method you > seem to be advocating is impossible 1. SPARK 2. Proving correctness of all program >>> proving correctness of contracts But the argument is bogus. If something is wrong it is wrong no matter how implementable it be. In fact, easily implementable wrong things are much more wrong than just wrong ones. (:-)) > (just like any user-input cannot be > guaranteed correct w/o either having all user-input as permissible, or > otherwise validating it) or difficult on the compile-time/static-analysis > level. Bingo! If you CANNOT impose precondition on it, then it is NOT a precondition. There is no contract violated when End_Error is raised by file Read. It is not the contract of Read to be supplied with infinite files! Since, the discussion is perpetually repeating itself, I will tell you your next turn: Ada I/O libraries are lousy, should have never used any exceptions. >> (Historically, pre-/post-conditions were invented by Dijkstra for the >> purpose of proving correctness. Later they were used for types to analyze >> substitutability issues etc.) > > And isn't the idea with Ada's constructs to at least aid proving the > correctness of a program? I heard different opinions on that. But since False => True, you could said so. Unfortunately it is also so that False => False... > Furthermore, wouldn't it be preferable to throw > an exception when the condition is violated? It would be a bug. The rule is simple: bug is when you cannot continue. Whatever you do having a bug is another bug. > That seems to fit perfectly > with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no? No, these are not contract violations. When they are pretended to be, they incur incredible harm. >>> If that was the case then, strictly speaking >>> JavaDoc's pre and postcondition annotating comments are superior to Ada's >>> pre and post condition because they don't implement anything and are, in >>> fact, just comments having no actual impact on the program text. >> >> Not if condition proof fault makes the program illegal. > > It does nothing, insofar as I know, regarding nprogram correctness. > http://en.wikipedia.org/wiki/Java_annotation has as an example the > "override" annotation which when violated only provides a warning. and? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de