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.196.232 with SMTP id ip8mr9061251pbc.6.1341478125415; Thu, 05 Jul 2012 01:48:45 -0700 (PDT) Path: l9ni10938pbj.0!nntp.google.com!news1.google.com!goblin1!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: Thu, 5 Jul 2012 10:48:50 +0200 Organization: cbb software GmbH Message-ID: <13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net> References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <13hfxjlq0xqtq.x3v8evyf4pku$.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-05T10:48:50+02:00 List-Id: 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. Yet another way: the language of contracts is not the object language: http://en.wikipedia.org/wiki/Object_language > 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. > 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? (:-)) >>> 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? >> 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, What about the statement: "Most Ada programs are best off not adding integer numbers caused by outright bugs"? The actual fallacy is in pretending that a bug can be handled. You can handle/be in only anticipated states. The proper statement should have been: "Ada is best to make the programmer aware of the states he might overlooked." >>> 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. Sure, because that is rubbish, and always was: http://en.wikipedia.org/wiki/Liar_paradox > [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. The contract language should deploy the intuitionistic logic. That is necessary anyway because some things are not provable. In the intuitionistic logic A or not A is not true (no law of excluded middle). E.g. "raise E" (I will raise E) and not "not raise E" (I may raise E. I don't promise not to rase E) are not equivalent statements. 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de