java - Could a final variable be reassigned in catch, even if assignment is last operation in try?

Question

I am quite convinced that here

final int i;
try { i = calculateIndex(); }
catch (Exception e) { i = 1; }

i cannot possibly have already been assigned if control reaches the catch-block. However, Java compiler disagrees and claims the final local variable i may already have been assigned.

Is there still some subtlety I am missing here, or is this just a weakness of the model used by the Java Language Specification to identify potential reassignments? My main worry are things like Thread.stop(), which may result in an exception being thrown "out of thin air," but I still don't see how it could be thrown after the assignment, which is apparently the very last action within the try-block.

The idiom above, if allowed, would make many of my methods simpler. Note that this use case has first-class support in languages, such as Scala, which consistently employ the Maybe monad:

final int i = calculateIndex().getOrElse(1);

I think this use case serves as a quite good motivation to allow that one special case where i is definitely unassigned within the catch-block.

UPDATE

After some thought I am even more certain that this is just a weakness of the JLS model: if I declare the axiom "in the presented example, i is definitely unassigned when control reaches the catch-block", it will not conflict with any other axiom or theorem. The compiler will not allow any reading of i before it is assigned in the catch-block, so the fact whether i has been assigned to or not cannot be observed.

Answer 1

JLS hunting:

It is a compile-time error if a final variable is assigned to unless it is definitely unassigned (§16) immediately prior to the assignment.

Quoth chapter 16:

V is definitely unassigned before a catch block iff all of the following conditions hold:

V is definitely unassigned after the try block.
V is definitely unassigned before every return statement that belongs to the try block.
V is definitely unassigned after e in every statement of the form throw e that belongs to the try block.
V is definitely unassigned after every assert statement that occurs in the try block.
V is definitely unassigned before every break statement that belongs to the try block and whose break target contains (or is) the try statement.
V is definitely unassigned before every continue statement that belongs to the try block and whose continue target contains the try statement.

Bold is mine. After the try block it is unclear whether i is assigned.

Furthermore in the example

final int i;
try {
    i = foo();
    bar();
}
catch(Exception e) { // e might come from bar
    i = 1;
}

The bold text is the only condition preventing the actual erroneous assignment i=1 from being illegal. So this is sufficient to prove that a finer condition of "definitely unassigned" is necessary to allow the code in your original post.

If the spec were revised to replace this condition with

V is definitely unassigned after the try block, if the catch block catches an unchecked exception.
V is definitely unassigned before the last statement capable of throwing an exception of a type caught by the catch block, if the catch block catches an unchecked exception.

Then I believe your code would be legal. (To the best of my ad-hoc analysis.)

I submitted a JSR for this, which I expect to be ignored but I was curious to see how these are handled. Technically fax number is a required field, I hope it won't do too much damage if I entered +1-000-000-000 there.