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 pz6mr4511174pbc.3.1340394119180; Fri, 22 Jun 2012 12:41:59 -0700 (PDT) MIME-Version: 1.0 Path: l9ni7940pbj.0!nntp.google.com!news2.google.com!goblin3!goblin1!goblin2!goblin.stu.neva.ru!news.stack.nl!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, 22 Jun 2012 14:41:55 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1340394118 9715 69.95.181.76 (22 Jun 2012 19:41:58 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 22 Jun 2012 19:41:58 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Original Date: 2012-06-22T14:41:55-05:00 List-Id: "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. And Ada *always* has had dynamic preconditions: procedure New_Line (Spacing : in Positive_Count := 1); Here, the precondition is "Spacing in Positive_Count". Your contention that a dynamic expression cannot be a precondition is the same as saying that no parameter can include a range (and thus ought be written as Count'Base above). ... > And implementations leaking into declarations is certainly a very bad > idea. This is NOT implementation; it's part of the contract. For the vast majority of subprograms, callers aren't supposed to call routines such that an exception is raised; it represents a bug. The only question is to whether those conditions are expressed in executable terms or in comments. For instance, the containers have operations like: procedure Insert_Space (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1); If Before is not in the range First_Index (Container) .. Last_Index (Container) + 1, then Constraint_Error is propagated. If Count is 0, then Insert_Space does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count; if the value of Last appropriate for length NL would be greater than Index_Type'Last, then Constraint_Error is propagated. {more text here} It would have much better if this was written as: procedure Insert_Space (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1) with Pre => (if Before not in First_Index (Container) .. Last_Index (Container) + 1 or else Container.Length > Index_Type'Last - Count then raise Constraint_Error); The latter is less likely to be misinterpreted, it still can be checked at run-time, the compiler can use it to completely eliminate redundant checks (which cannot be done for checks in the body absent of inlining -- which is usually a bad idea), and static analysis tools (and compilers, for that matter) can detect and complain about cases where the checks are known to fail (that is, where the program has bugs). And you get all of this without peeking into the body of the subprogram. We can't require the latter: it's beyond the state of the art to do that in most cases, but by doing this at runtime now, we get people writing these conditions so that as the state of the art improves more can be done for static detection. There never will be any static detection of conditions written as comments! Also note that in the above, this precondition is NOT part of the body (implementation) of the subprogram. This is required of all implementations -- it's part of the contract, not the part that varies between implementations. As such, it makes the most sense to write it as part of the contract. ... > Neither #1 nor #2 is defendable. 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" (that's the separation of specification from implementation). How your ideal language might work is irrelevevant in this forum. Please talk about Ada, not impossible theory. Randy.