Re: Contracted exceptions for Ada

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

On Mon, 10 Dec 2007 19:53:27 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:7m9wkymyi5h7.1235e72is9mp9.dlg@40tude.net...
>> On Fri, 7 Dec 2007 21:30:05 -0600, Randy Brukardt wrote:
> ...
>>> The ARG has discussed "exception contracts" a couple of times, but there
>>> didn't seem that there was enough interest. The problem was mainly that they
>>> simply don't look very valuable
>>
>> My observation is that a big deal of debugging Ada code is about tracing
>> down unexpected exceptions. I cannot give any figures, but it is extremely
>> frequent that a bug manifests itself as an exception propagation. Typically
>> Constraint_Error propagates where you didn't expect it. So the temptation
>> is to catch most of such things at compile time.
> 
> That's not going to be useful, since virtually any code that you can write
> *might* raise Constraint_Error,

Why is it a problem?

> and a lot of code *could* raise
> Program_Error, and everything *could* raise Storage_Error. There is no way
> to write a contract that doesn't contain those exceptions.

Program_Error is not my concern. Storage_Error can be fixed as I described
earlier.

And for all, what I meant under exception contracts was not about making a
program exception-free. It was about specifying which exception can
propagate and which cannot.

>>> Another one is what to do if a contract is violated. The obvious answer of
>>> raising Program_Error doesn't do anything other than lose information about
>>> an exception, so that isn't very satisfying.
>>
>> Yes, in my view exception contracts have to be static. (It makes no sense
>> to have run-time exception contracts. As well as any other contracts, there
>> is no any authority body to judge contract violations at run-time.)
> 
> OK, but that isn't going to happen in Ada. What you are looking for is a
> static analysis tool, like SPARK. That's especially true as you'll need
> static preconditions to have any hope of eliminating the Constraint_Errors
> (subtypes aren't powerful enough).

This is a separate issue. You seem to imply that the exception contracts
shall specify *when* an exception is raised or not. That is a much harder
problem and it indeed would require pre- and postconditions and cannot be
done in general case. What I am talking about is a much weaker framework
which only proves whether an exception cannot propagate. We do not need
pre-/postconditions for that.

A comparable case is exact real vs. interval arithmetic. We don't need
exact exception propagation analysis, we do a conservative *estimation* of.

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