Re: Contracted exceptions for Ada

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:185k0c8e598ko.16o5j2iv35zpn$.dlg@40tude.net...
> On Mon, 10 Dec 2007 19:53:27 -0600, Randy Brukardt wrote:
...
> > That's not going to be useful, since virtually any code that you can
write
> > *might* raise Constraint_Error,
>
> Why is it a problem?

Because every contract would have to include Constraint_Error, and that
would add a huge amount of verbiage to programs for no benefit. Or you have
to exclude it from the contract like Java does, which would be worse.

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

Program_Error *is* your concern. There is no way that a compiler could prove
that it would not be raised from a lot of code; as such it would have to be
included in the contract even though it isn't interesting to anyone
(presuming again static contract checking and no "unchecked" exceptions).

And your solution for Storage_Error adds a large number of new rules to the
language, and is unlikely to make it possible to eliminate the exception.
For instance, other tasks can allocate memory for the heap, so the only
possible way to tell if you are out of heap memory is to catch the
exception -- anything else is a race. And Janus/Ada at least uses heap
memory to allocate virtually everything not statically sized: pretty much
anything other than an elementary object or "null;" can raise Storage_Error
in Janus/Ada. Besides, you say you don't want to add preconditions and the
like, and then you do exactly that to handle Storage_Error. Can't have it
both ways...

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

Right, but the predefined exceptions can always propagate. The only way to
prove that they don't is to do extensive static analysis, and that isn't
happening in the language.

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

Right, but a the only possible conservative estimate is that all code can
propagate Program_Error, Constraint_Error, and Storage_Error. Even
    exception
           when others => null;

can raise Storage_Error and Program_Error (from finalization). And if you
replace "null" with a subprogram call, you will probably introduce
Constraint_Error. Unless you do quite a bit of static analysis, you can't
prove *anything* useful about what exceptions can propagate.

Java solves this by excluding the predefined exceptions, but all that does
is makes the contracts useless -- you don't really know what might
propagate. I hardly ever have problems with user-defined exceptions like
Windows_Error or Not_Valid_Error (from Claw, as an example) propagating: the
"comment" contracts make it pretty clear what can happen, and expected
errors are quickly handled.

Without some sort of static analysis required, all access dereferences *can*
raise Constraint_Error, all integer assignments can raise Constraint_Error,
and so on. Since we want all Ada compilers to work the same (so code is
portable), you would have to define what exact rules you are allowed to use
for determining whether an exception is raised, and which ones you are not.
That is a significant effort, and is going to be hard for some compilers to
implement -- moreover, compilers that know more would have to be prohibited
from using it. None of that seems good.

                                         Randy.