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!news4.google.com!feeder.news-service.com!xlned.com!feeder7.xlned.com!news2.euro.net!newsfeed.freenet.ag!ecngs!feeder2.ecngs.de!194.25.134.126.MISMATCH!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool2.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: <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> <4beaf93a$0$6875$9b4e6d93@newsspool2.arcor-online.net> Date: Wed, 12 May 2010 23:57:57 +0200 Message-ID: <1u6ficvfjfreg$.16cmwyau8jkd9.dlg@40tude.net> NNTP-Posting-Date: 12 May 2010 23:57:54 CEST NNTP-Posting-Host: c18adfc3.newsspool2.arcor-online.net X-Trace: DXC=k?COah3D?E[YI9]OHn9o5^A9EHlD;3YcR4Fo<]lROoRQ8kFZ>[ X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:11570 Date: 2010-05-12T23:57:54+02:00 List-Id: On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote: > 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. A C programmer would tell you same story about merits of pointers, casts and preprocessor. >>> 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 If they can for *every* case, they are statically checkable, per definition. > (b) can guide the author of a client of a DbC component? I don't know what does it mean technically. Doesn't core dump guide programmers? Blue screens certainly do. > 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. char X [80]; // Don't use X[80], X[81], no matter etc. > (A DbC principle is that assertions are *not* a replacement > for checking input (at the client side).) Exactly. Assertion is not a check. You said this. >>> What is "breach of contract" in your world? >> >> A case for the court. > > What's the court (speaking of programs)? A code revision. > 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. Mathematics has nothing to do with this. It is about a clear distinction between a contract and a condition, how undesirable it could be but nevertheless it is a condition, which you, as a programmer are obliged to consider as *possible*. Eiffel gives you an illusion of safety. This is even worse than C, which openly declares "I am dangerous." Simply consider the following rule: my program shall handle each exception I introduce. Objections? Then consider exceptions from assertions. >>> How would you specify >>> >>> subtype Even is ...; ? >> >> Ada's syntax is: >> >> subtype is ; > > What will static and static be for subtype Even? No, in Ada is not required to be static. Example: procedure F (A : String) is subtype Span is Integer range A'Range; -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de