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!news4.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!83.128.0.11.MISMATCH!news-out1.kabelfoon.nl!newsfeed.kabelfoon.nl!xindi.nntp.kabelfoon.nl!news2.euro.net!newsfeed.freenet.ag!feeder.erje.net!news2.arglkargh.de!noris.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="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> Date: Wed, 12 May 2010 19:24:11 +0200 Message-ID: <4j73xhgimt6r$.pu55kne2p2w5$.dlg@40tude.net> NNTP-Posting-Date: 12 May 2010 19:24:08 CEST NNTP-Posting-Host: dcd60cde.newsspool1.arcor-online.net X-Trace: DXC=MJhR4Fo<]lROoR1<`=YMgDjhg2[OgT3@U=9b>[6LHn;2LCV>[k`9T4`Yd34 X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11563 Date: 2010-05-12T19:24:08+02:00 List-Id: 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. Which is there is no substantial difference between Eiffel precondition and C's if statement beyond syntax sugar, and that if-statement is less misleading. > 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. > 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. > And like Pascal said : “Eiffel is far more easier than SPARK” (you cannot > request every one to know SPARK, and you help them when you provide them > something like Eiffel). Yes, but you do not want to prove everything, which is impossible anyway. 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. IMO, Ada does not need Eiffel-like pre- postconditions, assertions etc. They add nothing to safety and thus to Ada. It would be enough to introduce raise when ; and close the theme. (Yes I heard the argument that one can use them in declarations. I don't think that is a good idea. I don't like exceptions from declarations.) 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de