Re: Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO

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

"Peter C. Chapin" <pcc482719@gmail.com> wrote in message 
news:46idnVdMEr8J5EXN4p2dnAA@giganews.com...
...
> Exception contracts are a huge, HUGE topic and one that shouldn't be 
> treated too lightly.

We've had this discussion within the ARG. It's pretty clear to me what the 
answers are (but others may not agree). See AI12-0017-1 for my take on this. 
(The ARG has not yet discussed this AI.)

The problem in other languages is requiring them everywhere -- I'm pretty 
certain that will never work. They're critical for properly defining 
reusable code, but I'm dubious that they have much value in "top-level" code 
(the stuff that is created to use those reusable libraries). Good reusuable 
libraries are very hard work, and the more help the compiler can give the 
better...

...
Consider:
> + Should exception contracts be enforced statically or dynamically?

Statically. Dynamic enforcement is a total can of worms with no real value. 
The real question is whether the enforcement can depend on 
implementation-properties (that is, if the implementation can optimize away 
a check, can that be used in enforcing the contract), or whether it has to 
remain portable.

> + Should exception contracts be enforced at all or only produce warnings 
> or logs?

That's worthless from an language perspective; pretty much the only value 
beyond the comments that we already use is static checking. Personally, I'm 
not interested in adding features to Ada that can't be used by an Ada 
compiler (but only be separate tools).

> + What about backward compatibility with the existing code base? We don't 
> want to force people to decorate all code with exception contracts before 
> it will compile again with Ada 2020 (or whatever). Do we?

Clearly, the default has to be "raises anything", we can't make everything 
incompatible. As best as we can tell, the root problem in C++ and Java is 
that the default is more restrictive. (Stupid coding policies probably don't 
help, either.)

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

IMHO, no. The biggest value to these contracts is proving that 
language-defined exceptions don't occur (the compiler knows far more about 
this than any tool can figure out, as only it knows whether or not a check 
is generated for a particular operation in the code). The only exception 
that defies most such proofs is Storage_Error (and it can be eliminated in 
specialized circumstances). So I think everything should be specified. In 
order to cut down the size of such contracts, I've proposed allowing 
creating "sets of exceptions", so that only the single name of the set need 
be mentioned.

> + How should exception contracts interact with generic code?

I don't see any real problem here; a formal subprogram has to have an 
optional contract, and if it does, it has to "match".

> + Should exception contracts be a part of a subprogram's type? Consider 
> access to subprogram values and their usage.

Access-to-subprograms are probably going to always be "raises anything". 
This is very similar to the way preconditions work; one might expect that 
access-to-subprograms should allow preconditions and require some sort of 
matching, but that's just too complicated so it's purely dynamic.

This will mean that access-to-subprograms won't be able to be called from 
inside of exception contracted subprograms. But the only effect of that will 
be to encourage avoiding access-to-subprogram completely (a very positive 
result, IMHO, you can't prove anything about a call to an 
access-to-subprogram in Ada 2012 and I doubt that will change).

> + How should exception contracts interact with other static analysis 
> techniques? For example if a subprogram has a contract that says it might 
> raise exception E, but if static analysis can prove that a particular 
> usage will not actually raise E, does the programmer have to declare a 
> contract on the calling subprogram about E? One objection I've heard about 
> exception specifications in Java is that they require programmers to 
> either specify (or handle) exceptions that "clearly" can never actually 
> arise at that particular program point.

See my answer to the first question. I strongly lean toward the 
implementation-defined static check (I'd be against adding the contracts at 
all if that isn't the case), but I'm pretty certain that is going to be a 
tough sell (it will harm portability, as a compiler that isn't as "smart" 
may not be able to tell that the exception isn't raised).

The alternative of mandating what Ada compilers are required to be able to 
deduce is unlikely to work; it would be fiendishly complex and would add a 
great burden to at least some implementations. (Which would cause a lot of 
resistance, I think.)

> Now that Ada has preconditions the last point is particularly acute. The 
> precondition on a procedure P might guarantee that a called subprogram 
> won't raise an exception that it might nevertheless declare in its 
> exception contract.

That would be wrong; the exception contract should not cover things included 
in the precondition. And if the precondition is necessary to prevent an 
exception from being raised by the body, then the subprogram specification 
should be declared so that the precondition cannot be ignored. (That 
shouldn't prevent the compiler from eliminating it if it is redundant, just 
that it should never be unchecked.)

> It would be really unpleasant if the programmer had to also add an 
> exception contract to P stating that it might raise an exception that the 
> programmer knows the precondition will prevent!

As above, that's not how I envision these things working. (But please keep 
in mind, most of this is my feverish musing and it hasn't been vetted by 
others yet.)

> This is just a sample of some of the issues involved in the subject. There 
> are those who have answers for all of these issues.

That would be me, editor of the ARG and the Ada Standard. ;-)

> That's great. But again I sincerely hope that if exception contracts are 
> ever seriously considered for Ada that the matter be given the deep 
> consideration it deserves.

I hope you don't think that I just wrote this up based on absolutely 
nothing -- I've been thinking about how this would work since we started 
working on Claw...and I've taken input from many members of the ARG. (As 
well as discussions on these topics that the ARG had for Ada 2005, and a 
lengthy e-mail thread that we had specifically on the topic of what Java did 
wrong here). We have not yet had a formal discussion on this particular 
proposal, and I'm certain that it isn't 100% correct at this point (I must 
have forgotten something!). But it's rather insulting to have someone claim 
that it hasn't been given proper consideration before making a proposal (or 
to imply that the ARG would simply adopt something without thinking about 
it).

                                                        Randy.