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 Path: g2news2.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!194.134.4.91.MISMATCH!news2.euro.net!newsfeed.freenet.ag!feeder.erje.net!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 10:41:03 +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> Reply-To: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="8323584-1988756859-1273653663=:21749" X-Trace: tigger.scc.uni-weimar.de 1273650517 21814 141.54.178.228 (12 May 2010 07:48:37 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 12 May 2010 07:48:37 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: Xref: g2news2.google.com comp.lang.ada:11543 Date: 2010-05-12T10:41:03+02:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --8323584-1988756859-1273653663=:21749 Content-Type: TEXT/PLAIN; charset=iso-8859-1 Content-Transfer-Encoding: 8BIT On Tue, 11 May 2010, Dmitry A. Kazakov wrote: > On Tue, 11 May 2010 18:05:42 +0200, Yannick Duch�ne (Hibou57) wrote: > > > While they can be compared in some way, there is indeed a big difference : > > Eiffel is runtime oriented, SPARK is static analysis oriented. > > A proof of correctness cannot be run-time. Incorrectness need no proof. Actually, there is a difference between partial and total correctness. A program is partially correct, if it produces the correct result in the case it produces any result. A partially correct program may run infinitely or abort with an exception, but when it does neither, you get the specified result. A totally correct program is partially correct *and* terminates in finite time *and* doesn't abort with an unhandled exception. So Eiffel programs seen to be partially correct, but lack any proof of total correctness. Which is OK for some applications. I would expect the autopilot of an airplane to be totally correct -- partial correctness wouldn't be too helpful. But there are plenty of applications, where a partially correct program would be a huge improvement over all the software we are currently using ... BTW, SPARK also only provides partial correctness, but no total correctness. While SPARK allows to prove that no exception is raised (*), it lacks the option to specify (and verify, of course) variants for WHILE-loops (**). Eiffel supports such invariants. So long Stefan P.S.: I have worked a bit with SPARK, and I am currently trying to improve my knowledge about it. While I do prefer static analysis over Eiffels dynamic checking at run time, I still think Eiffel's approach has its place. The constraints of SPARK as a programming language are severe. (For me, the worst is the prohibition of recursive subprograms.) ------ (*) Actually, as much as I understand SPARK, it doesn't allow to prove that the absence of Storage_Error. For that purpose, one needs an additional compiler-specific tool. (**) I just read that the most recent version of SPARK is able to deal with generics. Great! Maybe, SPARK has also recently learned how to specify and prove loop variants? -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------ --8323584-1988756859-1273653663=:21749--