Re: Contracted exceptions for Ada



"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> writes:

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

I think what I proposed was more like what you say below:

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.

Right -- an iterator needs to be able to say "I can raise anything
raised by the loop-body procedure that is passed in to me."
That's one thing missing from Java, which makes exception
contracts more painful than they need to be. Passing a procedure to an
iterator causes the compiler to lose useful information.

I think preconditions could help a lot in this general area -- instead
of saying "I might raise Divide_By_Zero" on the divide procedure, one
can specify exactly what circumstances cause that exception --
Divide_By_Zero will be raised if and only if you try to divide by zero.
Then if at the call site, you divide by X, and X is Positive, there's
no need for a handler. Unfortunately, there's no Non_Zero subtype.

- Bob
.