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,UTF8 Path: g2news2.google.com!news3.google.com!feeder.news-service.com!newsfeed00.sul.t-online.de!newsfeed01.sul.t-online.de!t-online.de!news.belwue.de!newsfeed.arcor.de!newsspool4.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="utf-8" Content-Transfer-Encoding: 8bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH 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> Date: Wed, 12 May 2010 20:33:43 +0200 Message-ID: <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> NNTP-Posting-Date: 12 May 2010 20:33:39 CEST NNTP-Posting-Host: 9a6bf61a.newsspool1.arcor-online.net X-Trace: DXC=FR1=E2nlF;bUoRk[hk2Walic==]BZ:afn4Fo<]lROoRa<`=YMgDjhgbXeEk@>I_9Lh[6LHn;2LCVn[ On Wed, 12 May 2010 20:09:49 +0200, Georg Bauhaus wrote: > On 12.05.10 19:24, Dmitry A. Kazakov wrote: >> On Wed, 12 May 2010 18:06:16 +0200, Yannick Duchêne (Hibou57) wrote: >> >>> Well, I've noted you do not like runtime-check because it is not [formal] >>> proof of anything, but no one said it is formal proof, this is just better >>> to catch error the sooner and understand why this was an error. >> >> Yes, it is better but that is not the point. > > Being better is precisely the point (of DbC). > DbC talks about proof obligations, not about provability. Who is obliged to whom in what? >> there is no >> substantial difference between Eiffel precondition and C's if statement >> beyond syntax sugar, and that if-statement is less misleading. > > "If" is > - much more flexible and > - totally unspecific and > - not integrated with, e.g. rescue clauses; > - needs bodies > > You can emulate anything with "if" or write assembler, though ... . Yes, but all above is not substantial. >>> About expression now, although understandability of a source does not >>> provide proof, this help to at least make partial assertions and discover >>> what's wrong. >> >> No more than an appropriately placed if-statement, tracing call, debugging >> break point etc. > > You cannot place an "if" in a specification. The answer was in my post. You have skipped out. OK, it was that exceptions from declarations is not a good idea. And considering it more deeply, Eiffel cannot do it either, because specifications are static things. What you meant is actually "if" in declarations elaboration, which is quite possible. >>> It is best to >>> face an error like “this class invariant was violated” than “this access >>> to this memory address failed”. >> >> The text used in error message is up to the programmer. My objection is not >> that what Eiffel offers is useless. The objection is that it has nothing to >> do with contracts (in its normal meaning) or with design by. These are no >> more than *debugging* tools. Using the terms pre-, postcondition, invariant >> is also misleading. > > What is "breach of contract" in your world? A case for the court. >> What Ada lacks is better contracts specified by the programmer only when he >> wishes to. E,g, exception contracts, statements about purity of a function, >> upper bound of stack use etc. > > Raising of exceptions is an integral part of DbC specs. And buffer overflow is an integral part of C... I meant static contracts, statically checked, if that was not clear. It don't need a shortcut for if-then-raise. >> Ada had dynamic constraints long before Eiffel. If one wished to extend >> this feature, it is welcome. Just do not call it "error check", when you >> use the subtype Positive. Tie it to subtypes. > > How would you specify > > subtype Even is ...; ? Ada's syntax is: subtype is ; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de