The JLS spec for definite assignment is
not conservative. The following program (noted in the jacks test
suite) is required to be accepted by
a compiler but it reads an uninitialized variable and
therefore cannot verify.
The jacks test suite requires a compiler to reject this
code, but I'm not sure under what JLS clause it could do
so.

        void m(int i) {
            switch (i) {
               case 0:
                final int j;
                j = 1;
                class Local {
                    int k = j;
                }
                break;
               case 1:
                // Javac 1.4 compiles this, and causes a VerifyError
                int k = new Local().k;
            }
        }
       }