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.227.67 with SMTP id ry3mr8213242pbc.8.1341454716018; Wed, 04 Jul 2012 19:18:36 -0700 (PDT) MIME-Version: 1.0 Path: l9ni10938pbj.0!nntp.google.com!news1.google.com!goblin3!goblin2!goblin.stu.neva.ru!newsfeed.x-privat.org!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: Wed, 4 Jul 2012 21:18:24 -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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341454711 1595 69.95.181.76 (5 Jul 2012 02:18:31 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 5 Jul 2012 02:18:31 +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-04T21:18:24-05:00 List-Id: "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. But that's never, ever been true in Ada. Exactly. You claim that there cannot be such a thing as a dynamically enforced contract. But that's simply bogus - Ada has had those since the beginning of time - they were called "constraints". Failing one of these checks means that your program is wrong. Ada of course defines what happens (raising an exception, etc.), but handling those does not make your program less wrong. The only reason that these aren't detected statically is the difficulty (and impossibility, in some cases) of detecting them statically. Yes, of course, there are also exceptions raised for reasons outside of a contract (that is, those that don't appear in the profile of a subprogram), and handling those might make sense in a correct program. But handling exceptions raised for contracts does not make the program any less wrong; indeed, the only legitimate reasons for handling those is to make debugging easier [and, in a few applications, to make the application "bullet-proof"]. >> 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". > But also there are important consequences for software engineering. Since > these checks have nothing to do with contracts, they must be considered as > a part of the program semantics and all possible outcomes must be > *handled*. The problem of buffer overflow is exactly in pretending that it > cannot overflow. So the program is broken when it does. That's certainly a fallacy in general. Most Ada programs are best off *not* handling exceptions caused by outright bugs, because the Ada runtime will do a better job of pinpointing the source of the error than any facility you could create yourself. Of course, some programs have to be bullet-proof, but that is the tiny minority. In a sense, of course, it's the Ada runtime that's providing the "handling" of those bugs (runtime contract failures). And that means a programmer doesn't have to, unless they need bulletproof code that is resistent to bugs. A lot of programs are *not* in this category. The Janus/Ada compiler, for instance, makes no attempt to handle such bugs -- it's much better to abandon the compilation attempt immediately rather than producing a program based on guessing what was intended. >> I suppose you have a totally different definition of "correctness checks" >> than I do; as usual, we can't have a useful discussion because you have >> your >> own set of terminology. > > Terminology is secondary to the semantics. The problem is with the > meaning. Right. I recall in the past that you've been unwilling to grasp the idea of bugs being detected at runtime. Just because Ada defines what happens in those cases does not suddenly make it OK to introduce bugs into a program. >> SPARK is next to useless for real programs - at best it can be used only >> to >> prove small parts of a program, and it takes a lot of effort to get >> there. > > You don't need to prove every possible aspect of the program. The language > should allow the programmer to choose. Ada 83 had provable contracts > stated > in terms of types. Nothing prevents us from having more detailed contracts > as well as other program correctness stuff. I simply don't understand > where > is a problem with that. That's what we're trying to do, and you *obviously* have a problem with that. Learning more languages and more tools to do what an Ada compiler ought to be able to do is silly. >> Instead of getting the benefits of building in Ada now, >> and getting more and more static checks as compilers improve. > > I don't see tracking down exceptions as a benefit. Neither would it be a > for the maintainer to discover that the program suddenly became illegal > because static checks has been "improved." That's not a real problem, because any such program is already wrong (its depending on the failure of a dynamic contract). Sure, people can write such code, but it's just like overlaying objects using address clauses -- it might work, but its still wrong and there is no guarentee that a newer compiler version will not break such things. [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. OTOH, compilers can and do remove most of those canonical checks, and letting the contracts be enforced against whatever is actually raised by the generated code would be much more useful. But it is impractical to specify the checks that have to be removed (and not very helpful - it could only be a very small number), so what is raised has to be implementation-defined. Which means that just because a contract works on one compiler does not mean that it will work on another compiler (including a later version of the same compiler). I agree with you that runtime detection of exception contract failure makes no sense, so the only choices are implementation-defined or non-existent.] Randy.