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,UTF8 Path: g2news2.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.141.40.65.MISMATCH!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 12 May 2010 20:09:49 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.1.9) Gecko/20100317 Thunderbird/3.0.4 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> In-Reply-To: <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Message-ID: <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 12 May 2010 20:09:50 CEST NNTP-Posting-Host: 9da0ceac.newsspool2.arcor-online.net X-Trace: DXC=QV_RBmW_akY=>bdbdS?M0YA9EHlD;3YcR4Fo<]lROoRQ8kFZLh>_cHTX3j]N3^XD]i9nEW X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11565 Date: 2010-05-12T20:09:50+02:00 List-Id: 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. > 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 ... . >> 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. If you say Precondition: Has-Such-And-Such; then this is effectively raise when not Has-Such-And-Such; Except that smart tools do not need to understand the full program including its bodies in order to infer a precondition. >> 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? Anything that is not yielding a full proof of everything is a debugging tool. So what? Should we therefore bend the normal, worldly definition of "contract" to mean something that can never be had? > 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. Purity: postcondition: interesting_1 = interesting_1'old and interesting_2 = interesting_2'old and ...; Stack usage: precondition: avail = max_avail - 140; > 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 ...; ?