Contracted exceptions for Ada (was: Exceptions)

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

On Fri, 7 Dec 2007 21:30:05 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:uvkiadiwrfh2.wi288ebeq18y.dlg@40tude.net...
> ...
>> When "a way to force" reads "exceptions contract", then the answer is no,
>> there is no way, alas.
> 
> 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.

(Maybe a wild guess, but this could save Ariane V. A program assumed
Constraint_Error exception free was recompiled for the hardware where that
was not the case.)

> (for Ada, I'm not going to comment on other
> languages) when the details are looked at, and they'd be fairly complex to
> define. The biggest issue is compatibility, of course (since Ada has had
> exceptions from the beginning, and never has had contracts, they'd have to
> be optional - but it's not clear if optional contracts are worth much).

I don't see a problem here. Legacy code will have an implied exception
contract stating that anything may propagate out.

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

> (Static detection of contract
> violations isn't possible in general because the contracts have to be
> optional.) 

It is not optional it is "any exception may propagate."

> And then there is the problem of predefined exceptions like
> Storage_Error -- every routine *can* raise Storage_Error, although few
> *expect* to do so (if they don't allocate memory). Does that have to be
> included in every contract?

That's up to the programmer's choice. If he chooses to contract
Storage_Error as non-propagating, then be it so.

I think there exist ways to provide much better control over Storage_Error
than we have and without distributed overhead. The contract on
Storage_Error would be conditional. That is - the subroutine Foo does not
raise Storage_Error if there is N1..Nn bytes of free space in the storage
pools P1..Pn. Such contracts are conservatively checkable. Of course, the
actual pool states themselves will never be checked at run-time (following
the principle above).

In extraordinary cases the programmer should have a option to give his word
that a subprogram or a part of require no more than N bytes. That would be
an "unchecked Storage_Error contract", by analogy to Unchecked_Conversion:

function Recursive (...) return ... is
   -- I give my word that Recursive uses only 10K of stack
begin
   if ... then
      return Recursive (...);
   else
      return ...;
   end if;
end Recursive;

> If so, that's ugly, and if not, the oddity of
> not quite a contract is unpleasant. And there are more issues: the
> maintenance cascade when an exception is added or removed;

No problem. Exception contracts should be inheritable. File open would say
"I raise this and that and also anything disk driver does." (I remember
Robert Duff proposed that once.)

> what about
> call-back routines (think Process in the Containers library); and so on.

Conditional contracts: container's Forall is exception E free if Process
is.

> I'm sure that something could be worked out, but it seemed like there were
> more valuable things to do.

Like multiple dispatch? (:-)) 

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