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.220.230 with SMTP id pz6mr14848886pbc.3.1341621798540; Fri, 06 Jul 2012 17:43:18 -0700 (PDT) MIME-Version: 1.0 Path: l9ni11017pbj.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.ecp.fr!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 19:43:08 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net> <13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341621795 17009 69.95.181.76 (7 Jul 2012 00:43:15 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sat, 7 Jul 2012 00:43:15 +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-06T19:43:08-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net... > On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: >> ... >>>> Legality has nothing to do with preconditions or postconditions. >>> >>> => It is OK to violate a "contract" defined by these. Here you are. >> >> No, it's not OK; that is the crux of our disagreement. You seem to think >> that the only kind of "contract" is some sort of static thing. > > Exactly. Because the contract exists *before* any programs implementing it > and after them. The contract exists even when there is no such program. > Therefore it cannot depend on the program state. > > Another way to understand this: a contract describes states of a program. > As such it cannot depend on them. That's not my meaning of "contract". It doesn't have anything specific with "program states" (whatever the heck you mean by that -- I can't assume any reasonable interpretation because you make up terminology all the time). > Yet another way: the language of contracts is not the object language: We're not interested in other languages here (this is an Ada forum, after all); Ada is the *only* language worth talking about. So by your definition, nothing you are talking about is even relevant. Why do you bother? (Why do *I* bother? ;-) ... >> But that's never, ever been true in Ada. > > I already said that type constraints are not contracts. E.g. an actual > value of the discriminant does not create a new contract. The contract > covers *all* possible values of the discriminant. > >> Exactly. You claim that there cannot be such a thing as a dynamically >> enforced contract. > > Absolutely. How could you enforce a contract which has been *already* > violated? If a program reaches an illegal state, it is in that state. > Period. Illegal /= Wrong. An illegal state cannot be reached because you can't compile the program. An incorrect state can be reached simply by violating a check or contract. >> But handling exceptions raised for contracts does not make the program >> any >> less wrong; > > Really? What is the purpose of the exercise? Raising exception, rolling > the > stack, finalizing stuff, and so on only to resign that the program is as > wrong as it was before? (Maybe it is even *more* wrong than it was? (:-)) Practicality -- it's not possible to find all program errors before a program is fielded. And a lot of programs cannot fail - so that they have to have a failback position even when they self-detect that they are internally incorrect. It doesn't make the program any less wrong, but it keeps the system up so the plane still can land or you can still retrive files for www.ada-auth.org. But if you *could* have detected the "wrong" program earlier, you surely would have wanted to, so you could have eliminated the incorrect state. A whole lot about programming language design is about practicality and not about ivory tower exercises. Languages which are purely ivory tower exercises rarely have been used off of a college campus. >>>> The only kind of correctness checks that *can* exist in general are >>>> dynamic. >>>> Ada's entire reason to exist is to include checks like range checks and >>>> overflow checks to programs. Without them you get the buffer overflows >>>> and other errors that plague C code. >>> >>> Yes, but irrelevant. These checks are not contract checks, because, >>> otherwise you are in contradiction. No words can change that. >> >> Certainly not if you insist on using an unnecessarily limiting definition >> of >> "contract". > > Yes, the contract as opposed to the implementation limits the former not > to > be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada > 2012 "contracts" are implementations [POV #1]. Do you? No, because I use a very different definition of these terms. Contract is roughly equivalent to (Ada) specification. Implementation is roughly equivalent to (Ada) body. No caller should *ever* depend in any way on "implementation". (Ada screws this up for exceptions and tasking behaviors like blocking and abort.) The only things a caller can depend upon is that which is given in the specification. And that includes both dynamic and static parts. Tools which depend in any way on the contents of Ada bodies (other than the one they are processing) are limiting and violate the philosophy of Ada. Thus we have to get more machine-processable information into the Ada specification, so tools can process calls without having to violate separation by looking at the implementation (that is, the body). ... > The actual fallacy is in pretending that a bug can be handled. You can > handle/be in only anticipated states. Really? That's certainly not true of my web server or many other programs. exception when Err:others => Log_Error (Err); Reset_to_Known_Good_State; The above is that the bottom of most of my tasks. I have no idea what state the task is in when it gets to this handler; it certainly represents an "unanticipated state" in that any state that I actually anticipated has its own handlers and recovery mechanisms. But this handler works to recover the processing in 99% of the cases (good enough for this application); whatever caused the problem is abandoned, and it resets to handle another command. I suppose you'll twist the terminology around in some bizarre way to claim that an unanticipated state - which is the only way to reach this handler - is somehow anticipated simply because I can write a handler for it. That's of course nonsense - whatever I (or any other programmer) thought of is what I anticipated, and there is no way for an outside observer to know anything about those. So you cannot reason about those in any useful way - it's an irrelevant qualifier. >> Right. I recall in the past that you've been unwilling to grasp the idea >> of >> bugs being detected at runtime. > > Sure, because that is rubbish, and always was: > > http://en.wikipedia.org/wiki/Liar_paradox I don't get it. Just because you cannot detect *all* bugs -- that is, that you can't ever make a statement that a program is bug-free -- does not mean that you cannot detect *some* bugs. Indeed, this misguided focus on absolutes has prevented most practical progress in this area. And you're trying hard to prevent progress as well. I'm obviously wasting my time discussing this with you, so I'm done. (If I can resist, I'm surely going to try.) Randy. ... >> [As an aside, this means you do not want real exception contracts, since >> they cannot usefully be done without having it be implementation-defined >> when an exception is raised by a predefined check. The canonical >> semantics >> of Ada would require assuming that every line raises Storage_Error, >> Program_Error, and usually Constraint_Error -- that would make it >> virtually >> impossible to eliminate those exceptions from contracts. > > I don't see it as a big problem. There is a difference between an > obligation to raise exception and a possibility that an exception could be > raised. No one cares about an "obligation to raise an exception"; I can't imagine including those in exception contracts. (Indeed, any such "obligations" should be in the precondition or subtype predicates, so they never even reach the body of the subprogram.) The only contracts of interest are the "possibility that an exception could be raised", as those probably depend on outside effects (user input, file system results, etc.) ... > The vendors could gradually reduce the number of cases where E may be > raised without making clients relying on weaker contracts illegal. The > second cannot be misused to prove that E is raised. It just does not > follow > from the second, and conversely. I don't see this at all. Once you call a routine that has a contract that says "E might be raised", you have to include "E might be raised" in your contract as well. This "poisoning" is the major objection to exception contracts in practice. Moreover, if you have a language-defined check that raises E in a subprogram S, then you have to include the "E might be raised" contract if you have any exception contract at all. That's where the legality comes in. If you allow that contract to be omitted if the compiler can prove that the language-defined check will not fail (and this is common), then you have an implementation-defined legality check. If you *don't* allow that contract to be omitted, then you will have to include such a host of "E might be raised" contracts on every subprogram that no one would ever use the feature. (There are at least 8 common exceptions that could occur in large chunks of my code; and almost no code could be without Constraint_Error, Program_Error, and Storage_Error.) I'm pretty certain that the only useful exception contract would have to allow check elimination to affect legality -- and that's definitely a problem for some. (And they might even be right.) But my feeling is that it would be very valuable to specify that a routine does *not* raise Constraint_Error, and have the compiler verify (or refute) that fact. Randy.