Re: Exception contracts for Ada?

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

"Peter C. Chapin" <pcc482719@gmail.com> wrote in message 
news:XYadnZrAFoJvLUXN4p2dnAA@giganews.com...
...
>>> + 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.

There is no other possibility. One could imagine a restriction that required 
a contract on every subprogram. But as we found out with "overriding", that 
way lies dragons.

My personal opinion is that what Java got wrong was the default. "anything 
can be raised" is much friendlier than making people stick junk handlers in 
everywhere or change their contracts repeatedly. Some interfaces have to be 
designed in stone (like those for Claw, Ada.Containers, etc.), but most 
don't need that level of contracting.

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

Right; here again, this is what Java got wrong. By making the default "no 
exceptions", the contracts got immediately out of hand. And they then fixed 
that by excepting some exceptions from the contracts, making the contracts 
like swiss cheese. They never worked their way out of the morass -- proving 
again that two mistakes don't make something usable. :-)

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

No, the preconditions/predicates should prevent it from being raised, and 
the compiler should be able to prove that. So it doesn't need to be in most 
of the contracts. (If a Claw subprogram raises Constraint_Error, it's a 
bug!)

To me this is a big benefit of these contracts: you can *declare* exception 
absence, and the compiler will either prove it or fail to the code -- no 
restrictive and separate tool like Spark needed for that. (Which brings that 
particular benefit of Spark to everyone.)

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

Yes, of course. Otherwise, they're "raise any". But perhaps we won't do this 
any more than we do it for preconditions. (As far as I can tell, this 
prevents any proofs of a generic unit before instantiation, and makes the 
proofs "fragile" as a different instance might fail. This is not Ada to 
me...)

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

Right, and I'm pretty sure this is wrong (but too hard to fix, as it would 
require "matching" of arbitrary expressions - conformance is close but it 
doesn't work because the types would be different).

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

More is needed for preconditions, too, unless you never want to prove 
anything and make only dynamic checks. My guess is that access-to-subprogram 
is inherently unsafe from a proof perspective, and nothing is going to fix 
that. So there is no point in adding lipstick to a pig -- especially if the 
attempt to do so would make the entire proposal too complex (a real problem 
in Ada language proposals).

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

I think that the "solution" is that the "proof" is implementation-defined 
for language-defined checks. Which means that a program with "static" 
exception contracts might not be portable to a "dumb" compiler. That's 
annoying, but I think any alternative is going to turn out much worse (but 
I'm happy if someone wants to try to prove me wrong). Certainly, trying to 
define checks that have to be optimized away is going to be madness, and not 
using the knowledge that the compiler has is also madness. After all, 
"canonical semantics" says that
            A : Integer := 10;
might raise Constraint_Error, but I'd be amazed if there is any compiler 
that generates a check in this case.

I think only "implementation-defined" is likely to work. This is clearly the 
weak point of my proposal (and any useful exception contracts, IMHO).

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

I don't think it's time will ever come, simply because trying to do so will 
take up a lot of time and effort. I really have no idea how to describe that 
formally that could be understood (look at 11.6 to see how well that has 
been explained in past standards :-).

                                       Randy.