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!news3.google.com!feeder.news-service.com!newsfeed.straub-nv.de!news-2.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: GNAT packages in Linux distributions Date: Thu, 13 May 2010 02:37:37 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: 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> Reply-To: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: tigger.scc.uni-weimar.de 1273707914 8029 141.54.178.228 (12 May 2010 23:45:14 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 12 May 2010 23:45:14 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1aeof68v367bj$.1pps94zw5zmpd.dlg@40tude.net> Xref: g2news2.google.com comp.lang.ada:11573 Date: 2010-05-13T02:37:37+02:00 List-Id: 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. Yes, there are some applications where the exception is just as bad as the wrong answer. One such example could be the autopilot of a plane. The plane may crash because the autopilot stops working, or because the autopilot acts on wrong results. Crash is crash. But not all applications have that severe requirments. In fact, event he autopilot may benefit from checks -- if these are performed when the plane is still on the ground, and if any failed test prevents the plane from starting. > 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. > {Any Precondition} > raise Program_Error; > {Postcondition} Yes, that program is partially correct. Well, Hoare did originally not bother with exceptions, but the following program is partially correct even in the old we-do-not-know-about-exceptions sense: {Any Precondition} while false loop null; end loop; {Postcondition} > 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. 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! You don't even need to perform any static analysis to ensure their correctness. (But you must not turn of the checks!) Of course the catch is that you would rather want to specify postconditions which exclude exception propagation. I.e., you would need formal postconditions *without* the "or else propagate something" part. In Eiffel, there is no way to enforce such postconditions. And how should that be possible, without static analysis? Perhaps, the difference between SPARK and Eiffel DbC can be summarised as follows: -> 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. That doesn't mean that the contracts you can express in Eiffel are invalid, however. -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------