Re: Exception contracts for Ada?

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

On Mon, 24 Dec 2012 14:45:53 -0500, Peter C. Chapin wrote:

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

It must be so, even if the language were developed from scratch. The
problem is that exception checks are evidently undecidable. It means that
you must have a grey zone for the things you cannot prove either true or
false.

Of course some legacy stuff could be much better if contracted. E.g. a
promise not to raise anything in Finalize/Initialize, but that would indeed
break legacy code.
 
>>> + 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.

But a program is not required to have a specific exception contract. The
language should not enforce that. The default contract is: I can raise
anything.

>>> + 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?

Yes

> Will it be necessary to add syntax so that generic 
> formal parameters can have their exception contracts declared?

Possibly, e.g. formal exception, formal set of exceptions as generic
parameters.
 
> 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.

Sure, any [object] language aspect may have a generic counterpart [in the
meta language].

That should rather bother people pushing for more generics. To me it makes
little sense to invest any efforts into further developing of obviously
lousy concept.

>>> + 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?

This looks simple. When you declare an access to subprogram type, that
declaration will have an exception contract (possibly empty). E.g.

   type P is access procedure ... with exceptions => E1;

E1 is an exception contract. Now let you declare

   procedure F ... with exceptions => E2;

Then F'Access matches P if parameters do and E2 implies E1. Since contracts
are statically checked, you can check that at compile time.

[ A very useful thing for bindings, preventing passing Ada callbacks
raising exceptions to C libraries ]

> I do know that, in GNAT at least, preconditions can't be declared for 
> access to subprogram types.

For dynamic checks there is little difference anyway. I suppose 

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

Yes, that is the most difficult part of it, specification what is required
to be provable about exceptions = anything else is mandated to be
considered non-provable, even if you or compiler knows otherwise.

Although exception checks could be very, very conservative. I don't think
anything more sophisticated than what Ada mandates, for example, for
presence of return statements in the function body is required.

Static analysis could simply look after all calls the body does and merge
their contracts [so for any block having handlers]. One could refine this a
bit towards if- and case-statements with static expressions, but that is
not really needed, IMO.

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

The language, especially its type system, is full of such things. When you
do

   type T is new Integer;
 
then T is treated as another type, though you and the compiler know them
same.

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