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: a07f3367d7,23c0de5a42cf667e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!feeder.news-service.com!news-out1.kabelfoon.nl!newsfeed.kabelfoon.nl!bandi.nntp.kabelfoon.nl!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: GNAT packages in Linux distributions Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <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> <4beeea73$0$6883$9b4e6d93@newsspool2.arcor-online.net> Date: Sat, 15 May 2010 22:33:42 +0200 Message-ID: <1bh4399u1mx7j.1cbtkeqbv2mdd$.dlg@40tude.net> NNTP-Posting-Date: 15 May 2010 22:33:42 CEST NNTP-Posting-Host: c2da38c6.newsspool3.arcor-online.net X-Trace: DXC=W>dS_P[aY6V<<0iRN7DLEQMcF=Q^Z^V3X4Fo<]lROoRQ8kFGkK\4fZ X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11646 Date: 2010-05-15T22:33:42+02:00 List-Id: On Sat, 15 May 2010 20:39:46 +0200, Georg Bauhaus wrote: > On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote: > >> 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? He learned that from the semantics of intervals, when he uses intervals he supposed to know what they are. When you write a precondition you use some premises. Consider primitive operations of the type T. You cannot describe T in terms of T. I.e. + cannot refer to +. So interval must be known to the programmer. >> 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. If it could, you would not need program anything. E.g. the result would be obtained statically. >>>>> 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. How do you measure the difference? >>> (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. This is what programming in Ada all about. Since the rest of the language is by large safe, the main problem is debugging exceptions. I would like Ada having contracted exceptions rather than run-time assertions producing more exceptions than we already have. >>> (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. Nope, the key feature of tracing is that it does not change the program's behavior. Assertions with handled exceptions do change it. It is a very poor debugging tool. I would prefer a decent debugger to run-time assertions. Make it remember the break conditions between runs. That would be helpful and consistent. >> You have to define "possible value": > > In the sense of DbC: values that client can pass without > violating the DbC contract. And contract is of course a predicate of that set of values? Nice circular definitions. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de