Re: Exceptions and out procedure arguments (using GNAT GPL)

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

On Fri, 22 Jun 2007 20:15:02 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> 
>> I didn't talk about formal correctness or pre-/postconditions, but if you
>> bring this topic in. What is so difficult in:
> 
> I had this in mind:
> "Actually I think that boils down to your [Adam Beneschan's] stand point
> on exceptions vs. program correctness. Mine is that any exception shall
> be a valid (correct) outcome.
> 
> "In other words, exceptions are a subject of DbC, they aren't a vehicle of. "
> 
> How, exactly, can exception be made a subject of DbC (other than
> banning them)?

By having contracted exceptions, obviously.

Heck, I am not an employee of Praxis, you know, so you'd better ask them. 
But if I were at their place, I would introduce the predicate 
propagated(e). For each e, exception, propagated(e) is true when e is being 
propagated. Trivially, each Ada statement has in its precondition

   forall e not propagated (e)

except for the first statement of an exception handler:

exception
   when Constraint_Error =>
       require propagated(Constraint_Error) and
            not (...other exceptions...);

For built-in operations like "+" we could have:

   function "+" (Left, Right : Integer) return Integer;
   ensure
      (Left + Right not in Integer'Range and propagated(Constraint_Error))
   or
      (Left + Right in Integer'Range and Result = Left + Right)

[and not propagated (Program_Error) and not propagated (Data_Error) ...)]

For raise:

   raise e;
   ensure propagated(e) [and not ...]

P.S. Robert Duff said on many occasions that Storage_Error could be 
propagated almost anywhere. That's better to change and he mentioned some 
ideas of how to do this. But Storage_Error is not a catastrophe for 
provability. Just don't mention it in the contracts, and *consequently* 
don't handle it because you could not.

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