Re: GNAT packages in Linux distributions

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

On Thu, 13 May 2010 02:37:37 +0200, stefan-lucks@see-the.signature wrote:

> On Wed, 12 May 2010, Dmitry A. Kazakov wrote:
> 
>> On Wed, 12 May 2010 20:10:26 +0200, stefan-lucks@see-the.signature wrote:
>> 
>>> 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. 
> 
> We clearly disagree on this point. 
> 
> Consider being new in a town, and asking how to go from, say, the railway 
> station to the market place. If we ask a guy who appears to be a local 
> person in our eyes, but is actually as foreing as we are, most people 
> would prefer an exception "sorry, I don't know the way" over the answer of 
> being directed into the wrong direction. If you think, the "sorry" is as 
> bad as the wrong direction, that is your problem, which I am not 
> interested in discussing any further. 

Consider another example. Let you have a word processor, which also
calculates frequencies of some words. After typing dozen pages of the
document, you remove a word (the last instance, occasionally), and the
processor crashes on zero divide trying to calculate its new frequency. I
bet you would prefer a rubbish frequency displayed.

The bottom line, the effect of an error is undefined. You cannot define any
reasonable action upon, UNLESS further information were available. Which is
equivalent to *specification* of a behavior. Once the behavior is defined,
it is no more an error, e.g. the frequency of an unused word is displayed
as an empty string. It is a mere requirement. If you don't know the answer,
say "I don't know", do not shoot.

>> 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 exception may just as well be raised when checking the postcondition. 

or from an if-statement placed by the programmer.

>>    {Any Precondition}
>>     raise Program_Error; 
>>    {Postcondition}
> 
> Yes, that program is partially correct. 

I wouldn't consider it as such.

> Well, Hoare did originally not bother with exceptions,

BTW Hoare, wasn't it actually Edsger Dijkstra?

>> The problem is that Program_Error does not satisfy postcondition.
> 
>> 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.
> 
> Now I see what you mean. You are asking for contracts which include 
> exception propagation. Yes, that would be nice to have. 

How could it be otherwise?

> Then you should like Eiffel, because this is what Eiffel actually does. In 
> Eiffel, the formal postcondition
> 
>   require P;
> 
> is a shortcut notation for the logical
>   
>   Postcondition: P or else (Postcondition_Violation propagating);
> 
> (whatever the name of the exception is), which is the real postcondition 
> of an Eiffel program. If Eiffel checks P at the end of the program, and 
> raises that exception when the check fails, then 
> 
>   Eiffel-programs are always correct!

Yes. Therefore a lazy programmer could write

   raise Postcondition_Violation;

and claim his salary.

> You don't even need to perform any static analysis to ensure their 
> correctness. (But you must not turn of the checks!)

Nice language, the program semantics depends on the compiler options. (We
have this in some places in Ada too, unfortunately)

> Of course the catch is that you would rather want to specify 
> postconditions which exclude exception propagation.

Yep.

>   -> Eiffel is a very expressive programming language, 
>      while SPARK is less expressive. 
> 
>   -> The language for contracts in SPARK is more expressive
>      than the language for contracts in Eiffel.

OK
 
> That doesn't mean that the contracts you can express in Eiffel are 
> invalid, however.

With the addition you made they are not. Once you remove
Postcondition_Violation (which can be done by a compiler switch), they
become invalid.

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