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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.223.73 with SMTP id qs9mr14851798pbc.7.1341623381144; Fri, 06 Jul 2012 18:09:41 -0700 (PDT) MIME-Version: 1.0 Path: l9ni11068pbj.0!nntp.google.com!news1.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!weretis.net!feeder4.news.weretis.net!nuzba.szn.dk!news.jacob-sparre.dk!munin.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Fri, 6 Jul 2012 20:09:32 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341623378 18233 69.95.181.76 (7 Jul 2012 01:09:38 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 7 Jul 2012 01:09:38 +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-07-06T20:09:32-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:l2v5ycmyjzk.11k6wbda0san5.dlg@40tude.net... ... > 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. They're only "complete and independent" if and only if "contract" includes dynamic contracts. Otherwise, there have to be three things (call the third one "specification", if you like). Because there are lots of things that don't belong to "implementation" (runtime checking of any sort, for instance), and there has to be somewhere to put them. But I suppose only your worthless terminology can be argued. In which case, the answer does not matter, because it is irrelevant to using Ada (or any other practical programming language, for that matter). >> 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 Proving complete correctness of a program is a pointless, impossible exercise. Real SPARK programs exclude such a large portion of the code, it's unlikely that they've actually proved anything of value. The only real hope is combining static and dynamic checks to improve the correctness of programs. (Absolutely nothing will cause programs to be 100% correct in practice -- why even try?) ... > 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! Certainly not. End_Error is clearly not part of the precondition of Read. Mode_Error, OTOH, might be. It doesn't help to take up straw men, you know. It's not possible to write contracts why all exceptions, for every possible exit condition of a subprogram. In *any* language. Nothing about this is about ALL. It's all about MOST. You continue to insist on arguing about ALL. No one cares about ALL, because it is impractical if not impossible. > 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. Huh? The problem is your insistence on straw men. The only contract that makes sense for Read is "might raise End_Error". There is no possible description of why. And no one anywhere ever said that End_Error should be in a precondition, and certainly not that all exceptions should be in a precondition. I've only said that SOME exceptions should be in a precondition, because violating them is a bug. And only the programmer can determine which makes sense for a particular subprogram -- there cannot be a hard rule about that. End_Error being raised by Read is perfectly normal. Mode_Error being raised by Read is a serious bug. So what? You seem to want hard rules, but that is not how anything works in the real world. After all, "everything is legal so long as you don't get caught" (Traveling Wilburys). ... >> 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. What harm? The program is wrong when these happen. It should be fixed if practical. If it cannot be fixed, Ada lets you handle them to recover - but this is not something that should be relied on. If there is a harm, it's that you can't tell between these used as a contract and these used as an implementation artifact (say, handling an overflow error). It would have been nice to differentiate, but that was not done in Ada 83 and it is way too late now. You could of course get that effect by eliminating all of the constraints from your program and using Preconditions and Predicates instead -- that would get all contract failures raising Assertion_Error. Randy.