[RFC] SPARK exceptional contracts

[clairedross]

Link to text of RFC: https://github.com/clairedross/ada-spark-rfcs/blob/spark-exceptional-contracts/considered/rfc-spark-exceptional-contracts.md

[pyjarrett]

It's worth including as part of this RFC, a review of Java's "checked exceptions," and possibly C++ exception specifiers. Both of these were regarded as mistakes, and C++ which usually doesn't deprecate syntax, deprecated and even removed them. I think it's critical this proposal include how it's going to mitigate the issues especially associated with checked exceptions in Java.

[yannickmoy]

@pyjarrett The main issue with checked exceptions was that they needed to be accounted for on every direct and indirect caller, which caused a local change to have potentially a huge impact. I agree that, whatever the solution, you should not be forced to describe exceptional behavior, especially if you can show that no such behavior can arise for a given call. That certainly warrants discussion in the RFC.

[clairedross]

Hi Paul,

On Wed, Jan 5, 2022 at 2:46 PM Paul Jarrett @.***> wrote:

It's worth including as part of this RFC, a review of Java's "checked exceptions," and possibly C++ exception specifiers. Both of these were widely regarded as mistakes, and C++ which usually doesn't deprecate syntax, deprecated and even removed them. I think it's critical this proposal include how it's going to mitigate the issues especially associated with checked exceptions in Java.

I don't know much about these features, but they do not seem to have exactly the same goal. From what I could gather, C++ exception specifiers were used to do some optimization at compile time (right?). They were considered non friendly because they: (A) had little benefits in terms of optimization but for throw () (B) were not enforced at compile time (C) where hard to maintain because a change in the throw is a calle has to be propagated to the caller.

Here (A) does not apply, we need them for verification, not optimization. For (B), we propose to enforce them dynamically/statically by proof. For (C), yes, this is True, and unfortunately the annotation burden is often the price to pay to do formal verification... Also, if we go for the alternative proposal with Exceptional_Cases, we could have an others case to say that other exception can be raised in some cases without stating which (at the price of not having the information for formal verification obviously). -- Claire Dross Senior Software Engineer, AdaCore

[pyjarrett]

1. @clairedross, I agree. Ensuring you all had looked at Java Checked Exceptions was my major point, the reference to exception specifiers was to dissuade Ada compiler writers (I understand this is a SPARK RFC) from deciding to support the Exceptional_Cases aspect in that way. There were some interesting ideas from that time, and it's neat to see this RFC and the alternative, would allow an expansion on, and even provable form of exception guarantees.

2. @yannickmoy, the Contract_Cases version also seems fine given the rigor expected by SPARK code. I like the idea of being able to specify the precondition of when a subprogram will return an exception, but I'm not sure if that is always possible. It seems a bit weird conceptually to know when an exception would be thrown and still call the subprogram anyways, and seems like it would encourage rather than simply allow, exception use as a normal error handling mechanism.

[clairedross]

After both some internal and some external input, we have decided to put the Exceptional_Cases aspect as the main proposal.