How to determine whether the following examples are definitely assigned?

Question

Given the following examples:

class A {
    public static void main(String[] args) {        
        int n=5;
        int k;
        while(n<6) {
            k=5;
            break;
        }
        System.out.println(k);
    }
}

and:

class B {
    public static void main(String[] args) {                
        int  k;
        while(true) {
            k=5;
            break;
        }
        System.out.println(k);
    }
}

I know that the first example won't run properly because k hasn't been definitely assigned; while the second example can run through.

I also read the rough explanations given to a large number of examples in the earlier part of Chapter 16 of the JLS.

However, when I tried to use the formal definite assignment rules to judge these two examples, I was unable to make an accurate judgment on them.

The rules I'm using are from the JLS:

16.2.10 The while statement

• V is [un]assigned after while (e) S (§14.12) iff V is [un]assigned after e when false and V is [un]assigned before every break statement for which the while statement is the break target.

• V is definitely assigned before e iff V is definitely assigned before the while statement.

• V is definitely unassigned before e iff all of the following are true: – V is definitely unassigned before the while statement. – Assuming V is definitely unassigned before e, V is definitely unassigned after S. – Assuming V is definitely unassigned before e, V is definitely unassigned before every continue statement for which the while statement is the continue target.

• V is [un]assigned before S iff V is [un]assigned after e when true.

For example, when I'm judging the second example, if e is true, it seems that only the last rule can be applied, but this rule doesn't seem to be able to determine that k has been definitely assigned.

So, how can we determine whether the above examples have been definitely assigned according to the specifications?Thank you for reading and answering.

Answer 1

Out of all the bullet points, only the first one is the only relevant one, in order to determine whether System.out.println(k); at the end is valid.

V is [un]assigned after while (e) S (§14.12) iff V is [un]assigned after e when false and V is [un]assigned before every break statement for which the while statement is the break target.

The phrases "[un]assigned after e when true" and "[un]assigned after e when false" are special technical terms defined towards the start of the chapter. "[un]assigned after e when false" can still be a true statement even if the value of e is true.

From 16.1.1,

V is [un]assigned after any constant expression (§15.29) whose value is true when false.

So in the second example, both of the following holds:

• k is unassigned after true when false
• k is assigned after true when false

The point of this clause is to capture the idea of vacuous truth.

Obviously, it is also the case that k is definitely assigned before every break statement, so we can conclude that k is definitely assigned after the while statement, and k is not definitely unassigned after the while statement.

For the first example, "k is unassigned after n < 6 when false" holds, because k is unassigned before n < 6. "k is assigned after n < 6 when false" does not hold. See the sections 16.1.7 and 16.1.10 for more details. Therefore, k is not definitely assigned after the while statement, and also not definitely unassigned after the while statement.