System.in, System.out, System.err fields are incorrectly treated as immutable in Java

[wandernauta]

The following Java class verifies:

import java.io.InputStream;
import java.lang.System;

class Example {
    public static void example(InputStream foo) {
        if (System.in != null && foo != null) {
            InputStream a = System.in;
            System.setIn(foo);
            InputStream b = System.in;

            assert(a == b);
        }
    }
}

However, the assertion does not hold in real programs for legacy reasons, per JLS; these three specific fields have very special "a bit static final but not really static final" behavior that the compiler is aware of.

[bobismijnnaam]

One way to fix this would be to encode in, out and err as methods which have only \result != null as postcondition. This reflects real world behaviour nicely, meaning not being allowed to use them in contracts as they can change at any time, and assuming they change if you refer to them twice. It does require some extra fiddling in the frontend to get vercors to recognize these fields as special, but that is to be expected I guess. Too bad it will make the langspecifictocol pass more complicated...

[wandernauta]

That makes sense. Though, I was looking at that \result != null postcondition as well - the real System class doesn't seem to make that promise, this succeeds (does not verify):

class Example {
    public static void main(String[] args) {
        System.setOut(null);
        assert(System.out == null);
    }
}

Is it enough for setIn, setOut, setErr to @require this to make sure that nobody ever calls it with null?

[bobismijnnaam]

Yes, if these setters are really the only way to change the special fields, making the contracts of the setters require non-null arguments should be sufficient.