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!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!news-1.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: Wed, 12 May 2010 20:10:26 +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> 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 1273684681 29448 141.54.178.228 (12 May 2010 17:18:01 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 12 May 2010 17:18:01 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1p87qdlnjbufg.127laayhrw9x3$.dlg@40tude.net> Xref: g2news2.google.com comp.lang.ada:11562 Date: 2010-05-12T20:10:26+02:00 List-Id: On Wed, 12 May 2010, Dmitry A. Kazakov wrote: > Any program is partially correct, if otherwise has not been observed. I > fail to see how Eiffel is different from C or Assembler in that respect. In C, if I try to compute the factorial of a (natural) number, I'll always get an answer (assuming a decent program, which can be written by a first-year computer science student, and a normal C-compiler). The answer may be right or wrong. If the input is too large, the answer actually is wrong (our first-year student stores the result in an int variable, and 100! is too large). But I still get an answer, even if it is wrong. 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. In SPARK, the examiner (or the simplifier or the proof checker) will tell me that my program is only correct if I specify a certain precondition (e.g., if the input is less than some upper bound). So in SPARK, I can be sure that I'll get the right answer, and SPARK forces me to specify the proper preconditions to get the right answer. Except that even a proper SPARK program might run in an infinite loop ... In any case, there is a huge difference between SPARK and Eiffel, but also between Eiffel and C. > The point is that run-time checks contribute nothing to correctness either > partial or not. Because a partially incorrect program remains partially > incorrect independently on whether you check that or not: Technically, any program of the form {Any Precondition} Statements; if not Postcondition then raise Program_Error; end if; {Postcondition} is partially correct, even if "Statements;" are semantic nonsense (as long as the whole thing compiles at all), regardless of "{Any Precondition}". Perhaps you don't like raising an exception? OK, we can stick with the original approach from Hoare from 1969, who didn't know (or didn't care) about exceptions. The following program is partially correct, regardless of the "Statements;" and "{Any Precondition}": {Any Precondition} Statements; while not Postcondition loop null; end loop; {Postcondition} Actually, the second program could be written in SPARK. It would pass all the static verification performed by the SPARK toolset chain, without leaving any unproven verification conditions. Still, when running the program I can only trust that if I get a result, it satisfies my precondition -- but I can't be sure it satisfies my precondition. More natural -- but not necessarily better -- is the following program: {Any Precondition} while not Postcondition loop Statements; end loop; {Postcondition} Same problem: partial correctness is trivial, regardless of "Statements;". Stefan -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------