Re: GNAT packages in Linux distributions

[stefan-lucks@see-the.signature]

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. 

Yes, there are some applications where the exception is just as bad as the 
wrong answer. One such example could be the autopilot of a plane. The 
plane may crash because the autopilot stops working, or because the 
autopilot acts on wrong results. Crash is crash. But not all applications 
have that severe requirments. 

In fact, event he autopilot may benefit from checks -- if these are 
performed when the plane is still on the ground, and if any failed test 
prevents the plane from starting.

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

>    {Any Precondition}
>     raise Program_Error; 
>    {Postcondition}

Yes, that program is partially correct. 

Well, Hoare did originally not bother with exceptions, but the following 
program is partially correct even in the old 
we-do-not-know-about-exceptions sense:

  {Any Precondition}
  while false loop 
    null;
  end loop;
  {Postcondition}

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

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!

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

Of course the catch is that you would rather want to specify 
postconditions which exclude exception propagation. I.e., you would need 
formal postconditions *without* the "or else propagate something" part. In 
Eiffel, there is no way to enforce such postconditions. And how should 
that be possible, without static analysis?

Perhaps, the difference between SPARK and Eiffel DbC can be summarised as 
follows:

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

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


-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------