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: Wed, 12 May 2010 20:53:45 +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> <4beaeeed$0$6888$9b4e6d93@newsspool2.arcor-online.net> <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> In-Reply-To: <1c8dan2pi7bm9.1os0h56b9fukv$.dlg@40tude.net> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Message-ID: <4beaf93a$0$6875$9b4e6d93@newsspool2.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 12 May 2010 20:53:46 CEST NNTP-Posting-Host: 9da0ceac.newsspool2.arcor-online.net X-Trace: DXC=DVnNAMA1>VVFm0Y?OE@2^XA9EHlD;3YcR4Fo<]lROoRQ8kFZLh>_cHTX3j]0ChIO[KWOPT X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11569 Date: 2010-05-12T20:53:46+02:00 List-Id: On 12.05.10 20:33, Dmitry A. Kazakov wrote: >> Being better is precisely the point (of DbC). >> DbC talks about proof obligations, not about provability. > > Who is obliged to whom in what? By being a programmer subscribing to the principles of DbC, you are obliged to show that the components of your system obey the components' contracts. The compiler and run-time try to help you achieving this goal. >>>> 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. Which set of "specifications" has only static things in it? Why exclude conditionals whose results cannot reasonably be computed by the compiler but (a) can be computed for every single case occuring in the executing program (b) can guide the author of a client of a DbC component? For example, assume that Is_Prime(N) is a precondition of sub P. Furthermore, TIME(Is_Prime(N)) >> PERMISSIBLE_TIME. Then, still, PRE: Is_Prime (N) expresses an obligation, part of a contract: Don't call P unless N is prime, no matter whether or not assertion checking is in effect. (A DbC principle is that assertions are *not* a replacement for checking input (at the client side).) >> What is "breach of contract" in your world? > > A case for the court. What's the court (speaking of programs)? >>> 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 wasn't clear to me that you wanted a mathematically closed structure to be the only legitimate substance of "contract". I'm a programmer. If I "design" anything, it is a program whose parts need to interact in a way that meets some almost entirely non-mathematical specification. I try to add some formality to the whole thing. This helps. I wish I had static type checking for a start! >> How would you specify >> >> subtype Even is ...; ? > > Ada's syntax is: > > subtype is ; What will static and static be for subtype Even?