I'm trying to quickly write up a tool to compute the transitive closure of all possible exceptions resulting in an invocation to a given method. Checked exceptions are an interesting means by which to attempt compiler enforcement of this. In Java, for example, exceptions that could be thrown are well known primarily because of strict inheritance rules, removing uncertainty by disallowing overriding methods to declare that they throw new exception types (aside from strengthening through polymorphism). The fact that you must either catch or declare that you throw an exception is simply a way to instruct the compiler what you intend to throw or let seep through the cracks. Arguably it could probably do a decent job (clearly not 100%, though) at figuring it out without requiring you to explicitly state it, however. And then perhaps it just becomes a compiler warning when you don't catch something.

Anyhow, I'm trying to hammer out the logic for my program and I came up with this. It's a bit cryptic, and I've probably used some symbols in uncommon ways... oh well... it helped me to think through the situation, and will be a great help when I actually implement it.

To compute the transitive closure of possible exceptions thrown as a result of an invocation to a method:

Let d be the method in question and a tuple of <t^d,m^d>, where t^d is the static type being analyzed and m^d is the method handle. Let C(d) be the set of tuples <i^C(d)_i,t^C(d)_i,m^C(d)_i>, for i = 0 to |C(d)|, representing method calls reachable from within d’s IL body (regardless of certain code paths and/or code path probabilities—probabilistic analysis could be quite interesting, but is not the focus of this effort), where i^C(d)_i is the instance on which a method is being called (or e for static method calls), t^C(d)_i is the static type to which the method call refers, and m^C(d)_i is the method handle being called.

Let DirThrows (d) be the set of exception types for which an explicit throw instruction is present within d’s IL body.

[informative] RefThrows(d) is defined below to equal the set of exceptions that could be thrown as a result of invoking a method call inside of d’s body, transitively closed on C(d).

Let Exc(d) be the set of exception types that could by thrown as a result of invoking method d. Specifically, Exc(d) = { DirThrows(d) È RefThrows(d) | deleting any e for which d‘s body contains an enclosing exception handler that catches e or a base-type and does not issue a rethrow instruction }.

Let RefThrows(d) be union of all E_i computed as follows:

For each <i^C(d)_i,t^C(d)_i,m^C(d)_i> Î C(d)

If virtual(<t^C(d)_i,m^C(d)_i>) is false, let E_i = Exc(<t^C(d)_i,m^C(d)_i>).

Otherwise, if there exists an assignment to i^C(d)_i of type u within visibility that provides an implementation for which virtual(<u,m^C(d)_i>) is false or whose instance construction is also within visibility and that can be deterministically proven to be the last known assignment (i.e. non-pointer local variable), let E_i = Exc(<u,m^C(d)_i>).

Otherwise, let T be the set of known derivative types of t^C(d)_i. If |T| = 0, let E_i = Exc(<t^C(d)_i,m^C(d)_i>). Otherwise, let E_i = { the union of all Exc(<u,m^C(d)_i>) for each u Î T }.