Re: GNAT packages in Linux distributions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote:

> 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).
> 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. 

1. Wrong answer is no more/less incorrect as an exception. Otherwise you
have to introduce some scale of correctness, which is called accuracy. A
program can yield more or less accurate results staying correct.

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 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}".

No. If Statements were irrelevant, you could take this:

   {Any Precondition}
    raise Program_Error; 
   {Postcondition}

The problem is that Program_Error does not satisfy postcondition.

> Perhaps you don't like raising an exception? 

I don't like any action upon a failed check, if that was a check. To self
checks are clearly infeasible.

> OK, we can stick with the original approach from Hoare from 1969, who 
> didn't know (or didn't care) about exceptions.

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.

> The following program is 
> partially correct, regardless of the "Statements;" and "{Any 
> Precondition}":
> 
>   {Any Precondition}
>   Statements;
>   while not Postcondition loop 
>     null; 
>   end loop;
>   {Postcondition}

Hmm, I would consider it totally incorrect => not partially incorrect,
because in no state it satisfies the postcondition.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de