Suggest only calls allowed in any state when the receiver's state is unknown

liquidjava-example/src/main/java/testSuite/ErrorStateHintConstructors.java

@@ -0,0 +1,55 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Each constructor creates the needed state, but only one that can be called is suggested
+@StateSet({"fresh", "ready"})
+public class ErrorStateHintConstructors {
+
+    @StateRefinement(to = "ready(this)")
+    public ErrorStateHintConstructors() {}
+
+    @StateRefinement(from = "ready(this)", to = "fresh(this)")
+    public void use() {}
+
+    // a concrete class: the constructor is suggested
+    static void concrete(ErrorStateHintConstructors value) {
+        value.use(); // Expect: State Refinement Error
+    }
+
+    // the receiver is this object, which a new object would not change
+    public void self() {
+        this.use(); // Expect: State Refinement Error
+    }
+}
+
+@StateSet({"fresh", "ready"})
+abstract class ErrorStateHintConstructorsAbstract {
+
+    @StateRefinement(to = "ready(this)")
+    public ErrorStateHintConstructorsAbstract() {}
+
+    @StateRefinement(from = "ready(this)", to = "fresh(this)")
+    public void use() {}
+
+    static void fail(ErrorStateHintConstructorsAbstract value) {
+        value.use(); // Expect: State Refinement Error
+    }
+}
+
+@StateSet({"fresh", "ready"})
+class ErrorStateHintConstructorsPrivate {
+
+    @StateRefinement(to = "ready(this)")
+    private ErrorStateHintConstructorsPrivate() {}
+
+    @StateRefinement(from = "ready(this)", to = "fresh(this)")
+    public void use() {}
+}
+
+class ErrorStateHintConstructorsPrivateUser {
+    static void fail(ErrorStateHintConstructorsPrivate value) {
+        value.use(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStateHintJoins.java

@@ -0,0 +1,40 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Joins of the states reached on different paths are not a lack of knowledge
+@StateSet({"closed", "opened"})
+@StateSet({"unlocked", "locked"})
+public class ErrorStateHintJoins {
+
+    @StateRefinement(to = "closed(this) && unlocked(this)")
+    public ErrorStateHintJoins() {}
+
+    @StateRefinement(from = "closed(this)", to = "opened(this)")
+    public void open() {}
+
+    @StateRefinement(from = "unlocked(this)", to = "locked(this)")
+    public void lock() {}
+
+    @StateRefinement(from = "closed(this) && unlocked(this)")
+    public void enter() {}
+
+    // every combination of the two state sets is reached on some path
+    public static void everyState(boolean p, boolean q) {
+        ErrorStateHintJoins d = new ErrorStateHintJoins();
+        if (p)
+            d.open();
+        if (q)
+            d.lock();
+        d.enter(); // Expect: State Refinement Error
+    }
+
+    // the paths differ in one of the two state sets the call checks, so both states are named in full
+    public static void oneSet(boolean p) {
+        ErrorStateHintJoins d = new ErrorStateHintJoins();
+        if (p)
+            d.open();
+        d.enter(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStateHintNaming.java

@@ -0,0 +1,59 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// The needed and current states are named only in the state sets that matter
+@StateSet({"created", "open", "ready"})
+@StateSet({"quiet", "loud"})
+public class ErrorStateHintNaming {
+
+    @StateRefinement(to = "created(this) && quiet(this)")
+    public ErrorStateHintNaming() {}
+
+    // a state of either set: each is named alone, not combined with every state of the other set
+    @StateRefinement(from = "open(this) || loud(this)")
+    public void read() {}
+
+    public static void use(ErrorStateHintNaming s) {
+        s.read(); // Expect: State Refinement Error
+    }
+}
+
+// every state allows flip(), each by its own refinement: a or b, not all six states
+@StateSet({"a", "b"})
+@StateSet({"x", "y", "z"})
+class ErrorStateHintNamingToggle {
+
+    @StateRefinement(to = "a(this) && x(this)")
+    public ErrorStateHintNamingToggle() {}
+
+    @StateRefinement(from = "a(this)", to = "b(this)")
+    @StateRefinement(from = "b(this)", to = "a(this)")
+    public void flip() {}
+
+    public static void use(ErrorStateHintNamingToggle t) {
+        t.flip(); // Expect: State Refinement Error
+    }
+}
+
+// known in one of three state sets: only that set is named
+@StateSet({"start", "canEdit", "end"})
+@StateSet({"undoable", "notUndoable"})
+@StateSet({"redoable", "notRedoable"})
+class ErrorStateHintNamingPartlyKnown {
+
+    @StateRefinement(to = "start(this) && notUndoable(this) && notRedoable(this)")
+    public ErrorStateHintNamingPartlyKnown() {}
+
+    @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)")
+    public void redo() {}
+
+    @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)")
+    public void undo() {}
+
+    @StateRefinement(from = "notRedoable(this)")
+    public void check() {
+        this.redo(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownAnyState.java

@@ -0,0 +1,28 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// reset() works in any state, so it is suggested even though the state is unknown; open() alone is not
+@StateSet({"created", "open", "closed"})
+public class ErrorStateHintUnknownAnyState {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintUnknownAnyState() {}
+
+    @StateRefinement(to = "created(this)")
+    public void reset() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+
+    public static void use(ErrorStateHintUnknownAnyState f) {
+        f.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/Reader.java

@@ -0,0 +1,26 @@
+package testSuite.classes.state_hint_checked_error;
+
+import java.util.Scanner;
+
+// A failed check of the receiver does not decide its state; a check of another object says nothing about it
+public class Reader {
+
+    public static void failedCheck(Scanner it) {
+        if (!it.hasNext()) {
+            it.next(); // Expect: State Refinement Error
+        }
+    }
+
+    public static void failedCheckOfTheSameScanner(Scanner scanner) {
+        Scanner same = scanner;
+        if (!scanner.hasNext()) {
+            same.next(); // Expect: State Refinement Error
+        }
+    }
+
+    public static void checkOfAnotherScanner(Scanner other, Scanner input) {
+        if (other.hasNext()) {
+            input.next(); // Expect: State Refinement Error
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hint_checked_error/ScannerRefinements.java

@@ -0,0 +1,17 @@
+package testSuite.classes.state_hint_checked_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"hasMore", "noMore"})
+@ExternalRefinementsFor("java.util.Scanner")
+public interface ScannerRefinements {
+
+    @Refinement("_ == true --> hasMore(this)")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore(this)", to = "noMore(this)")
+    String next();
+}

liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/Editor.java

@@ -0,0 +1,15 @@
+package testSuite.classes.state_hint_undo_manager_error;
+
+import javax.swing.undo.UndoManager;
+
+public class Editor {
+
+    static UndoManager history() {
+        return new UndoManager();
+    }
+
+    static void redoLast() {
+        UndoManager undoManager = history();
+        undoManager.redo(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java

@@ -0,0 +1,26 @@
+package testSuite.classes.state_hint_undo_manager_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// Issue #454: with an unknown state, redo() needs redoable, and the only call that leads there, undo(), needs
+// undoable, which is just as unknown
+@ExternalRefinementsFor("javax.swing.undo.UndoManager")
+@StateSet({"undoable", "notUndoable"})
+@StateSet({"redoable", "notRedoable"})
+public interface UndoManagerRefinements {
+
+    @StateRefinement(to = "notUndoable(this) && notRedoable(this)")
+    void UndoManager();
+
+    @StateRefinement(from = "redoable(this)", to = "undoable(this) && notRedoable(this)")
+    void redo();
+
+    @StateRefinement(from = "undoable(this)", to = "notUndoable(this) && redoable(this)")
+    void undo();
+
+    @StateRefinement(from = "redoable(this)", to = "return && redoable(this)")
+    @StateRefinement(to = "return ? redoable(this) : notRedoable(this)")
+    boolean canRedo();
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java

@@ -25,8 +25,8 @@ public enum Kind {
         PATH_DEPENDENT_STATE,
         /** The object is in a state where no call with a state refinement is allowed */
         FINAL_STATE,
-        /** The object's state is unknown, so these are the calls that lead to a state that allows the failing call */
-        REACHING_CALLS
+        /** The object can be in any state: the state the failing call needs, and the constructors that create it */
+        NEEDED_STATE
     }
 
     public static Hint general(String message) {