Re: Exception contracts for Ada?

["Peter C. Chapin" <pcc482719@gmail.com>]

I know there be dragons down this road, but I will comment on a few of 
your points. First, I want to emphasize that I'm not necessarily 
disagreeing with you... just elaborating on some ideas.

On 12/24/2012 11:34 AM, Dmitry A. Kazakov wrote:

>> + Should exception contracts be enforced statically or dynamically?
>
> Statically. Contracts cannot be enforced dynamically, it is rubbish.

I tend to agree that exception contracts should be enforced statically 
or else you end up with the mess C++ got itself into with its exception 
specifications. The problem of what to do at runtime if the contract is 
violated seems like a show-stopper for dynamic enforcement.

>> + What about backward compatibility with the existing code base?
>
> No problem at all. Empty (missing) contract = any exception may propagate.
> Everything would be 100% compatible.

But is that what we would want? I'm not sure.

>> + Should exception contracts distinguish between "impossible" exceptions
>> that shouldn't occur in a correct program (like Constraint_Error) and
>> "normal" exceptions that pertain to environmental problems such as
>> invalid input data?
>
> There is no such distinction.

Java does not require exception specifications for certain classes of 
exceptions such as for dereferencing null pointers and similar low level 
(language support) things. If it did then virtually every method would 
need to be decorated with an exception specification.

In Ada there are, for example, so many ways Constraint_Error can be 
raised that requiring it to be contracted by every subprogram seems... 
wrong somehow.

>> + How should exception contracts interact with generic code?
>
> As any other language thing does. Generic code has "generic contracts"
> which become normal contracts after instantiation.

The interesting part is not the contracts on the generic code itself but 
rather on the entities used by the generic code. Are exception contracts 
on generic code to be checked when the generic code is compiled or at 
instantiation time? Will it be necessary to add syntax so that generic 
formal parameters can have their exception contracts declared?

I suppose there are similar questions surrounding the interaction of 
pre- and postconditions and generic code. I'm not sufficiently up on Ada 
2012 yet to know how those issues are currently handled but I'm guessing 
that, because they are dynamic checks, the compiler doesn't worry about 
them.

>> + Should exception contracts be a part of a subprogram's type?
>
> There is no subprogram types in Ada so far.

If I call a subprogram indirectly via an access value, what do I know 
statically about its exception contract? How can I statically check that 
the exception contracts are being honored?

I do know that, in GNAT at least, preconditions can't be declared for 
access to subprogram types. Instead the preconditions are checked as the 
pointed-to subprogram is entered. I'm not sure if that's ideal but in 
any case it seems to make some sense for dynamically checked 
preconditions. For statically checked exception contracts, though, it 
seems like something more is needed.

> Do you mean the case when P calls to Q which is allowed to propagate E
> while P promises not to propagate E? In that case if analysis shows that P
> never propagates E, no special handler is required.

Yes that's basically what I mean. What you are suggesting sounds like it 
would require mandating a certain level of static analysis in compilers. 
Otherwise how could one write a portable program? I could imagine a very 
advanced compiler saying, "I can see that Q will never raise E in this 
situation but at the level of analysis mandated by the standard it would 
not be possible to tell that. Thus I'm going to require you to put a 
contract on P anyway declaring that P might raise E (even though you and 
I both know it won't) for portability to lesser compilers who will 
require it."

It seems to me that's a case where the standard is actively interfering 
with the capabilities of an advanced compiler.

On the other hand the idea of mandating some level of static analysis 
may be an idea who's time has come. I'm thinking again about pre- and 
postconditions. Specifying it would be difficult, I imagine.

Peter