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: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!feeder.news-service.com!kanaga.switch.ch!switch.ch!news.belwue.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Sat, 15 May 2010 20:39:46 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.1.10) Gecko/20100512 Thunderbird/3.0.5 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions References: <87mxw9x7no.fsf@ludovic-brenta.org> <16bz9kvbqa8y9$.155ntpwpwl29d.dlg@40tude.net> <4be97bea$0$2966$ba4acef3@reader.news.orange.fr> <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net> <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> <4beaf93a$0$6875$9b4e6d93@newsspool2.arcor-online.net> <1u6ficvfjfreg$.16cmwyau8jkd9.dlg@40tude.net> <4beb5dfa$0$6883$9b4e6d93@newsspool2.arcor-online.net> <1qvxyz4nolwsi.1fth5xpxi2m3t.dlg@40tude.net> <4bede0af$0$6883$9b4e6d93@newsspool2.arcor-online.net> <1ru2ex5e8d8y6$.jjts04h6mhb.dlg@40tude.net> In-Reply-To: <1ru2ex5e8d8y6$.jjts04h6mhb.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4beeea73$0$6883$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 15 May 2010 20:39:47 CEST NNTP-Posting-Host: 792d9f55.newsspool2.arcor-online.net X-Trace: DXC=WFD0j[]4aGi>jlK2>IgHGdA9EHlD;3Ycb4Fo<]lROoRa8kFejVh3D0NT^0FDhkbn@WeIa On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > No type system can express the program semantics. OK, lets keep this in mind. > Compute should have the contract: if the sequence A,B is sorted then ... > else Constraint_Error propagated. And of course, A, B is just an interval > [B, A], and should be declared as such: > > function Compute (X : Interval) return Number > with Precondition => True; OK, I guess we'd have a To_Interval (A, B) function raising constraint_error in case the programmer improperly passes A < B. Which he has learned not to do from some comment that states contractual obligations of client wishing to call To_Interval? >>> Note, since your "preconditions" are not static, >>> how can you know *what* they say, in order to do as they do? >> >> I can write my client code such that the preconditions are >> true. > > Really? What about: > > pre : not HALT(p) This is why I mentioned "not solve hard problems". I want to keep making sense in my preconditions/comments. > There is a reason why they aren't static. Practically, yes, there is a reason why normal programming cannot hope to rely on static analysis. >>>> IOW, no redundant checks. >>> >>> No, it would be *inconsistent* checks. No program can check itself. >> >> DbC checks are not part of the (intended) program. Monitoring can be >> turned off and this should have no effect on program correctness. > > and thus on program execution. q.e.d. The programs (with or without monitoring) are not too different and hence will lead to a useful program construction process. (Better exceptions.) >> (a) there is nothing the programmer knows about valid Index_80 >> values (viz. the odd ones) > > They are *all* valid, that is the contract of Careful. I guess we disagree here: I think that a "programming into exceptions" style leads to the universally applicable precondition True, but otherwise keeps the programmer in the dark about how to not make a subprogram raise. OTOH, being more specific (trying to explain additional "constraints") seems helpful. Here I recall "No type system can express the program semantics." Until Ada has a type system that can express expectations better than predicates, I'll rather have stupid, weakly typed predicates, supported by tools, than nothing. loop begin P(X); exit; exception when constraint_error => X := find_another_x; end; end loop; >> (b) there is no debugging hook that can be turned on >> or off (monitoring the precondition X rem 2 = 1). > > Debugging hooks do not belong to code. I guess my wording was too unspecific. Call it tracing automatism or whatever. > You have to define "possible value": In the sense of DbC: values that client can pass without violating the DbC contract.