Soundness: a field initialised in its declaration keeps that state in other methods, even after the constructor changed it #446

Impact: a protocol violation that crashes at runtime is accepted. When a field is initialised in its declaration (private Res res = new Res();), the state from that initialiser is used for the field in every method. That holds even after the constructor has moved the object to another state. Typestate on fields should start unknown in each method, as it does for a field assigned only in the constructor.

Minimal reproducer

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"open", "closed"})
class Res {
    @StateRefinement(to = "open(this)")
    public Res() {}

    @StateRefinement(from = "open(this)", to = "closed(this)")
    public void close() {}

    @StateRefinement(from = "open(this)")
    public void use() {}
}

public class Repro {
    private Res res = new Res();     // open here...

    Repro() {
        res.close();                 // ...closed once the constructor has run
    }

    void work() {
        res.use();                   // use() needs open: should be an error (or at least "unknown")
    }
}

Expected: an error at res.use(), since res is closed (or its state is unknown in work).

Actual (main @ f7f366c, and 1a506fe): Correct! Passed Verification.

Real-world scenario. GUI code keeps a javax.swing.undo.UndoManager in a field initialised at its declaration and configures it in the constructor. Here, with an external spec of UndoManager where setLimit is refused after end():

import javax.swing.undo.UndoManager;

public class U16_FieldInitEndedCanUndoSetLimit {
    private UndoManager undoManager = new UndoManager();   // initializer: the verifier keeps start here

    U16_FieldInitEndedCanUndoSetLimit() {
        this.undoManager.end();
    }

    void shrink() {
        if (this.undoManager.canUndo()) {          // true after end(); the verifier still believes start
            this.undoManager.setLimit(5);          // throws RuntimeException: setLimit after end()
        }
    }

    public static void main(String[] args) {
        new U16_FieldInitEndedCanUndoSetLimit().shrink();
    }
}

• On the JVM: java.lang.RuntimeException: Attempt to call UndoManager.setLimit() after UndoManager.end() has been called (UndoManager.java:289).
• LiquidJava (f7f366c), with the spec from co-specification (examples/undomanager/specs/4-tables-UndoManagerRefinements.java): Correct! Passed Verification.

Contrast: the same class with private UndoManager undoManager;, assigned in the constructor (this.undoManager = new UndoManager(); this.undoManager.end();), is correctly rejected at setLimit(5) (co-specification probe U13, on 1a506fe). Only the declaration initialiser leaks its state.