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

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

On Mon, 24 Dec 2012 10:49:39 -0500, Peter C. Chapin wrote:

> On 12/24/2012 06:13 AM, Yannick Duch�ne (Hibou57) wrote:
> 
>> This one is fine, I see your point now.
> 
> Exception contracts are a huge, HUGE topic and one that shouldn't be 
> treated too lightly. I can understand their attraction in a language 
> that prides itself on its suitability for robust programming. However, 
> if exception contracts are ever added to Ada I pray to the Ada gods (the 
> ARG?) that it is only done after an extensive review has been made of 
> the issues related to them in other languages. One only needs to search 
> for the topic of exception specifications in C++ and Java to find a 
> mountain of discussion on the subject. Consider:
> 
> + Should exception contracts be enforced statically or dynamically?

Statically. Contracts cannot be enforced dynamically, it is rubbish. What
would a violation of exception contract do? Raise another exception in
violation of what was already violated?

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

Considering it static, a violation would obviously make the program
illegal, no warnings, no code generated.

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

No problem at all. Empty (missing) contract = any exception may propagate.
Everything would be 100% compatible. Moreover, the nice thing is that you
could hang whatever contracts (preserving the functionality, of course) on
the existing legacy libraries (e.g. Ada containers, System etc) while
keeping all legacy code 100% compatible. So long the caller is not
contracted itself it can happily ignore any contracts of the callee.

> + 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. A distinction exists between exceptions
required to propagate and ones that are required not to propagate. You use
the former when you can prove more (e.g. Constraint_Error if argument of
sqrt is negative) and the latter when you cannot prove (enumerate, compute)
exceptional states non reachable (e.g. End_Error when EOF).

And again, contracting sqrt to raise Constraint_Error means nothing to its
caller. You can write

   if HALT(p) then
      Y := sqrt (-1.0);
   else
      Y := sqrt (8.0);
   end if;

This is not the problem of sqrt. Neither it is a problem for the caller
*until* it would try to promise not to raise Constraint_Error.

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

> + Should exception contracts be a part of a subprogram's type?

There is no subprogram types in Ada so far.

> Consider 
> access to subprogram values and their usage.

No difference to usual treatment of access types. The contract of an access
type includes contracts of implicitly dereferenced target type. This is the
case for access to array indexing, access to record members.
 
> + 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.

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.

[It is static. The problem exists if and only if checks are dynamic.
Dynamic checks are evil, always.]

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

There should be no dynamic preconditions. The issue, again, is only when
checks are dynamic. Dynamic checks are inherently inconsistent.

One of the advantages of contracted exceptions is that inconsistent dynamic
preconditions can be replaced with consistent exception contracts. E.g.

   Pre => X < 0
   Post => PP

with

   Pre => True
   Post => (X < 0 and raise Constraint_Error) or else PP

> This is just a sample of some of the issues involved in the subject.

More tricky are issues involving inheritance, contracts of primitive
operations as a whole (whether you allowed to manipulate them for the
overrides), Storage_Error and Program_Error.
 
> There are those who have answers for all of these issues. 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.

No less is expected from the ARG!

Merry Christmas,

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