Re: GNAT packages in Linux distributions

[stefan-lucks@see-the.signature]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 2441 bytes --]

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!  ------