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.190.104 with SMTP id gp8mr1603682pbc.4.1341291086260; Mon, 02 Jul 2012 21:51:26 -0700 (PDT) MIME-Version: 1.0 Path: l9ni10735pbj.0!nntp.google.com!news1.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!216.196.98.142.MISMATCH!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!novia!news-out.readnews.com!news-xxxfer.readnews.com!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.straub-nv.de!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: Mon, 2 Jul 2012 23:51:19 -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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1341291084 17794 69.95.181.76 (3 Jul 2012 04:51:24 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 3 Jul 2012 04:51:24 +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 X-Received-Bytes: 8100 Date: 2012-07-02T23:51:19-05:00 List-Id: (Note: I haven't yet read anyone else's response to this thread; but I thought I owed Dmitry a response. If this ground was previously covered, please feel free to ignore my response.) "Dmitry A. Kazakov" wrote in message news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net... > On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" wrote in message >> news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net... >>> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote: >>> >>>> "Dmitry A. Kazakov" wrote in message >>>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... >>>> ... >>>>> This is what constitutes the core inconsistency about dynamic >>>>> pre-/post-conditions. If they #1 implement behavior (e.g the stack >>>>> contract >>>>> to raise something when full), then they cannot be suppressed and do >>>>> not >>>>> describe the contract. If they do describe the contract #2, they may >>>>> not >>>>> implement it and thus shall have no run-time effect. >>>> >>>> You're right, but I don't see any inconsistency. They are clearly #1, >>>> and >>>> that includes all of the existing Ada checks as well. >>> >>> If you take a stance on #1, then checking stack full is no more >>> evaluation >>> of the precondition, which does not depend on the stack state anymore, >>> as >>> it of course should be. So the "true" precondition is just: True. >> >> Huh? This makes no sense whatsoever. >> >> We can't require static detection of precondition failures any more than >> we >> can demand static detection of range violations. > > You seem to imply that value in the range is a precondition of the > operation constrained to that range. This is wrong. It can't be "wrong", because the programmer of an abstraction decides what the preconditions and postconditions are. > If S is a subtype of T then the precondition is > > X in T > > The postcondition is > > (X in S and ) or (X not in S and Constraint_Error propagated) > >> And Ada *always* has had dynamic preconditions: >> >> procedure New_Line (Spacing : in Positive_Count := 1); > > The precondition here is Spacing in Positive_Count'Base because the > behavior of New_Line is *defined* when Spacing is not in > Positive_Count'Range. > > New_Line(0) > > is a *legal* Ada program. Legality has nothing to do with preconditions or postconditions. Preconditions and postconditions are two sides of the same coin. They're checks made on the way into and the way out of a subprogram. There is absolutely no justification for saying that these are different in some way. You are saying that only a postcondition can have dynamic components, which is nonsense. You seem to want to associate the actions of the precondition with the subprogram itself, but that is also wrong. Preconditions are checked *before* a subprogram is called, so those actions occur *before* anything in the subprogram (and thus anything in the postcondition to the subprogram). You're trying to fit all exceptions into a single box, which is silly. Some exceptions are clearly part of the preconditions of the subprogram -- the only reason that they are exceptions is because it is currently beyond the state of the art to check these statically. Any occurrence of these exceptions in a program represents a bug; they should never happen in a correct program. For instance, the mode check for a file. OTOH, some exceptions are reporting issues that only are detectable *after* the subprogram has been called (for example, the Use_Error caused when a disk is full). Those should be in the exception contract (not the postcondition; that's only for "normal" return; the exception contract might have a separate postcondition for each exceptional return). Deciding between these is something that only the designer of a subprogram can do. No mathematical theory can ever do that. ... >> Nothing you say on this topic makes any sense, at least from an Ada >> perspective. Here you are saying that Ada's entire design and reason for >> existing is "not defendable" > > Why entire? Dynamic correctness checks are not defendable, as demonstrated > on numerous examples. 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. Compile-time detection of bugs is only possible in very limited and not very useful cases. Limiting a programming language to those cases only makes it unusable (exhibit #1 - SPARK). 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. ... >> How your ideal language might work is irrelevevant in this forum. > > It is not mine language. It is a methodology of defining and proving > program correctness as introduced by Dijkstra. It applies to all languages > without exemption. We're not interested in "proving program correctness". That's (still) beyond the state of the art for any realistic programming language. We *are* interested in dynamic features that can provide information to future static analysis tools. But realistic analysis tools will never (and should never) try for "complete" analysis. >> Please talk about Ada, not impossible theory. > > The only impossible theory here is about meaning of dynamically checked > preconditions, e.g. #1 or #2? That is indeed impossible, because > inconsistent. Otherwise Dijkstra's approach works pretty well with any > language, e.g. SPARK does for Ada. 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. It's the sort of thing that turns programmers off (it *certainly* has done that to me!) and essentially pushes them to stick with the unsafe languages that they are using. Instead of getting the benefits of building in Ada now, and getting more and more static checks as compilers improve. This idea of "perfect" proving has essentially prevented these techniques from moving into the mainstream, and it is sad that this is the case. Anyway, if you are going to push "program proving", then we literally have nothing to talk about. So this conversation is done. Randy.