Re: GNAT packages in Linux distributions

[stefan-lucks@see-the.signature]

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