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!nf02.dk.telia.net!starscream.dk.telia.net!news.tele.dk!news.tele.dk!small.news.tele.dk!bnewspeer01.bru.ops.eu.uu.net!bnewspeer00.bru.ops.eu.uu.net!emea.uu.net!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> <1aeof68v367bj$.1pps94zw5zmpd.dlg@40tude.net> Date: Thu, 13 May 2010 11:09:41 +0200 Message-ID: NNTP-Posting-Date: 13 May 2010 11:09:37 CEST NNTP-Posting-Host: 77a916c3.newsspool2.arcor-online.net X-Trace: DXC=24Q37mdT`:D02Sh8E_NfIAA9EHlD;3YcB4Fo<]lROoRA8kF On Thu, 13 May 2010 02:37:37 +0200, stefan-lucks@see-the.signature wrote: > On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > >> On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote: >> >>> In Eiffel, I'll either get an answer, or the program will tell that at >>> some point of time when computing, say, the factorial of 100, a certain >>> exception has been raised. (I didn't try out Eiffel, but that is what I >>> would expect.) But if I get an answer, I can be sure it is the right one. >>> That is partial correctness. >> >> 1. Wrong answer is no more/less incorrect as an exception. > > We clearly disagree on this point. > > Consider being new in a town, and asking how to go from, say, the railway > station to the market place. If we ask a guy who appears to be a local > person in our eyes, but is actually as foreing as we are, most people > would prefer an exception "sorry, I don't know the way" over the answer of > being directed into the wrong direction. If you think, the "sorry" is as > bad as the wrong direction, that is your problem, which I am not > interested in discussing any further. Consider another example. Let you have a word processor, which also calculates frequencies of some words. After typing dozen pages of the document, you remove a word (the last instance, occasionally), and the processor crashes on zero divide trying to calculate its new frequency. I bet you would prefer a rubbish frequency displayed. The bottom line, the effect of an error is undefined. You cannot define any reasonable action upon, UNLESS further information were available. Which is equivalent to *specification* of a behavior. Once the behavior is defined, it is no more an error, e.g. the frequency of an unused word is displayed as an empty string. It is a mere requirement. If you don't know the answer, say "I don't know", do not shoot. >> 2. It is unrelated to error checks. The programmer did not use any. That >> Eiffel possibly checks for integer overflow and C does not is irrelevant to >> the issue. > > The exception may just as well be raised when checking the postcondition. or from an if-statement placed by the programmer. >> {Any Precondition} >> raise Program_Error; >> {Postcondition} > > Yes, that program is partially correct. I wouldn't consider it as such. > Well, Hoare did originally not bother with exceptions, BTW Hoare, wasn't it actually Edsger Dijkstra? >> The problem is that Program_Error does not satisfy postcondition. > >> His approach, which I greatly appreciate, is perfectly compatible with >> exceptions. Exception propagation is a part of the program behavior to be >> checked as anything else. E.g. >> >> pre : x = 1 >> if x = 1 then >> raise Foo; >> end if; >> post : Foo propagating >> >> This program were be incorrect if it would not raise Foo. > > Now I see what you mean. You are asking for contracts which include > exception propagation. Yes, that would be nice to have. How could it be otherwise? > Then you should like Eiffel, because this is what Eiffel actually does. In > Eiffel, the formal postcondition > > require P; > > is a shortcut notation for the logical > > Postcondition: P or else (Postcondition_Violation propagating); > > (whatever the name of the exception is), which is the real postcondition > of an Eiffel program. If Eiffel checks P at the end of the program, and > raises that exception when the check fails, then > > Eiffel-programs are always correct! Yes. Therefore a lazy programmer could write raise Postcondition_Violation; and claim his salary. > You don't even need to perform any static analysis to ensure their > correctness. (But you must not turn of the checks!) Nice language, the program semantics depends on the compiler options. (We have this in some places in Ada too, unfortunately) > Of course the catch is that you would rather want to specify > postconditions which exclude exception propagation. Yep. > -> Eiffel is a very expressive programming language, > while SPARK is less expressive. > > -> The language for contracts in SPARK is more expressive > than the language for contracts in Eiffel. OK > That doesn't mean that the contracts you can express in Eiffel are > invalid, however. With the addition you made they are not. Once you remove Postcondition_Violation (which can be done by a compiler switch), they become invalid. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de