Impact: a subclass's external spec can use the states of a @StateSet declared in its superclass's spec only if the verifier reads the superclass's spec first. Spec files are read in package order (file names here), so splitting a JDK hierarchy into one file per class breaks depending on the names. FrameRefinements.java sorts before WindowRefinements.java, so this fails.

Minimal reproducer (three files in one directory)

// FrameRefinements.java
@ExternalRefinementsFor("java.awt.Frame")
public interface FrameRefinements {
    @StateRefinement(to = "notDisplayable(this)")
    void Frame(String title);

    @StateRefinement(from = "notDisplayable(this)")
    void setUndecorated(boolean undecorated);
}

// WindowRefinements.java
@StateSet({"displayable", "notDisplayable"})
@ExternalRefinementsFor("java.awt.Window")
public interface WindowRefinements {
    @StateRefinement(to = "notDisplayable(this)")
    void dispose();

    @StateRefinement(to = "displayable(this)")
    void pack();
}

// Use.java
public class Use {
    static void borderless() {
        Frame host = new Frame("Playfield");
        host.pack();
        host.setUndecorated(true);
    }
}

Actual (main @ 19991d3):

Not Found Error: Ghost 'java.awt.Frame.notDisplayable' could not be found
6 |     @StateRefinement(to = "notDisplayable(this)")
  |                            ^^^^^^^^^^^^^^^^^^^^
FrameRefinements.java:6

If the two interfaces are in one file with Window first, or if WindowRefinements.java is renamed so that it sorts first (e.g. AWindowRefinements.java), the program verifies up to the expected State Refinement Error on host.setUndecorated(true).

Expected: the result does not depend on file order. The state sets of every external spec should be registered before any spec's methods are read. RefinementProcessor.processPackage already does this for the methods of user classes, but ExternalRefinementTypeChecker.visitCtInterface reads an interface's @StateSets and its methods together, one interface at a time. Sub-packages are processed after their parent, so the same problem appears when the two specs are in different packages.

Found while working on #456.