Return implies state

liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorRefinements.java

@@ -0,0 +1,25 @@
+package testSuite.classes.iterator_observer_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class):
+ * {@code hasNext} is an informative check (no state change), and {@code next} consumes one
+ * element, resetting state so a fresh check is required before the next consumption.
+ *
+ * <p>{@code java.util.Iterator} itself is an interface, and external refinements only attach to
+ * classes — Scanner gives us the same API in a class form.
+ */
+@StateSet({"hasMore", "noMore"})
+@ExternalRefinementsFor("java.util.Scanner")
+public interface IteratorRefinements {
+
+    @Refinement("_ == true --> hasMore(this)")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore(this)", to = "noMore(this)")
+    String next();
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java

@@ -0,0 +1,36 @@
+package testSuite.classes.iterator_observer_correct;
+
+import java.util.Scanner;
+
+public class IteratorUse {
+
+    public static void readOne(Scanner it) {
+        if (it.hasNext()) {
+            it.next();
+        }
+    }
+
+    public static void readTwo(Scanner it) {
+        if (it.hasNext()) {
+            it.next();
+            if (it.hasNext()) {
+                it.next();
+            }
+        }
+    }
+
+    public static void readInElse(Scanner it) {
+        if (!it.hasNext()) {
+        } else {
+            it.next();
+        }
+    }
+
+    public static void recursive(Scanner it) {
+        if (it.hasNext()) {
+            String s = it.next(); 
+            System.out.println(s);
+            recursive(it);
+        } 
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java

@@ -0,0 +1,62 @@
+package testSuite.classes.iterator_observer_error;
+
+import java.util.Scanner;
+
+public class IteratorMisuse {
+
+    // No check at all: state of the parameter is unknown.
+    public static void nextWithoutCheck(Scanner it) {
+        it.next(); // State Refinement Error
+    }
+
+    // Else branch of hasNext(): condition was false, so we know !hasMore.
+    public static void nextInElseBranch(Scanner it) {
+        if (it.hasNext()) {
+        } else {
+            it.next(); // State Refinement Error
+        }
+    }
+
+    // Negated check: !hasNext() true means hasNext returned false, so !hasMore.
+    public static void nextNotInElse(Scanner it) {
+        if (!it.hasNext()) {
+            it.next(); // State Refinement Error
+        }
+    }
+
+    // After consuming with next(), state becomes noMore — a second next() in the same
+    // then-branch must fail.
+    public static void doubleNextInThen(Scanner it) {
+        if (it.hasNext()) {
+            it.next();
+            it.next(); // State Refinement Error
+        }
+    }
+
+    // Empty if-then: the bug we fixed in visitCtIf would have masked this join, leaking the
+    // path-variable's truthiness past the if and silently asserting hasMore.
+    public static void nextAfterEmptyIf(Scanner it) {
+        if (it.hasNext()) {
+        }
+        it.next(); // State Refinement Error
+    }
+
+    // Sequential ifs: state is consumed by the first then-branch's next(), and the second if's
+    // path-variable assertion must not leak past its join.
+    public static void sequentialIfsLoseState(Scanner it) {
+        if (it.hasNext()) {
+            it.next();
+        }
+        if (it.hasNext()) {
+        }
+        it.next(); // State Refinement Error
+    }
+
+    // Empty if + empty else: neither branch establishes hasMore.
+    public static void nextAfterEmptyIfElse(Scanner it) {
+        if (it.hasNext()) {
+        } else {
+        }
+        it.next(); // State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java

@@ -0,0 +1,25 @@
+package testSuite.classes.iterator_observer_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+/**
+ * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class):
+ * {@code hasNext} is an informative check (no state change), and {@code next} consumes one
+ * element, resetting state so a fresh check is required before the next consumption.
+ *
+ * <p>{@code java.util.Iterator} itself is an interface, and external refinements only attach to
+ * classes — Scanner gives us the same API in a class form.
+ */
+@StateSet({"hasMore", "noMore"})
+@ExternalRefinementsFor("java.util.Scanner")
+public interface IteratorRefinements {
+
+    @Refinement("_ == true --> hasMore(this)")
+    boolean hasNext();
+
+    @StateRefinement(from = "hasMore(this)", to = "noMore(this)")
+    String next();
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java

@@ -0,0 +1,29 @@
+package testSuite.classes.state_test_method_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"aliveDone", "aliveNotDone", "notAlive"})
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+public interface AbstractUndoableEditRefinements {
+
+    @StateRefinement(to = "aliveDone(this)")
+    void AbstractUndoableEdit();
+
+    @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)")
+    void redo();
+
+    @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)")
+    void undo();
+
+    @StateRefinement(from = "!notAlive(this)", to = "notAlive(this)")
+    void die();
+
+    @Refinement("_ == true --> aliveDone(this)")
+    boolean canUndo();
+
+    @Refinement("_ == true --> aliveNotDone(this)")
+    boolean canRedo();
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java

@@ -0,0 +1,23 @@
+package testSuite.classes.state_test_method_correct;
+
+import javax.swing.undo.AbstractUndoableEdit;
+
+public class EditCycler {
+    public static void undoIfPossible(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.undo();
+        }
+    }
+
+    public static void redoIfPossible(AbstractUndoableEdit edit) {
+        if (edit.canRedo()) {
+            edit.redo();
+        }
+    }
+
+    public static void redoIfPossible() {
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        edit.canRedo();
+        edit.undo();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java

@@ -0,0 +1,26 @@
+package testSuite.classes.state_test_method_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"aliveDone", "aliveNotDone", "notAlive"})
+@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
+public interface AbstractUndoableEditRefinements {
+
+    @StateRefinement(to = "aliveDone(this)")
+    void AbstractUndoableEdit();
+
+    @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)")
+    void redo();
+
+    @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)")
+    void undo();
+
+    @Refinement("_ == true --> aliveDone(this)")
+    boolean canUndo();
+
+    @Refinement("_ == true --> aliveNotDone(this)")
+    boolean canRedo();
+}

liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java

@@ -0,0 +1,95 @@
+package testSuite.classes.state_test_method_error;
+
+import javax.swing.undo.AbstractUndoableEdit;
+
+public class EditMisuse {
+
+    public static void undoInElseBranch(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+        } else {
+            edit.undo(); // State Refinement Error
+        }
+    }
+
+    public static void undoNotInElse(AbstractUndoableEdit edit) {
+        if (!edit.canUndo()) {
+            edit.undo(); // State Refinement Error
+        }
+    }
+
+    public static void wrongTesterForRedo(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.redo(); // State Refinement Error
+        }
+    }
+
+    public static void wrongTester2() {
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        edit.undo();
+        if (edit.canUndo()) {
+            edit.undo();
+        }
+        edit.undo(); // State Refinement Error
+    }
+
+    // Two undos in the same then-branch: condition forces aliveDone for the first, but the second
+    // is in aliveNotDone.
+    public static void doubleUndoInThen(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.undo();
+            edit.undo(); // State Refinement Error
+        }
+    }
+
+    // Nested ifs: outer canUndo => aliveDone, inner canUndo => aliveDone (still), so calling
+    // redo() in the inner then is illegal (redo needs aliveNotDone).
+    public static void nestedIfRedoFromAliveDone(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            if (edit.canUndo()) {
+                edit.redo(); // State Refinement Error
+            }
+        }
+    }
+
+    // Sequential guarded undos with no else: after the first if, state is aliveNotDone in BOTH
+    // paths (then took canUndo=>aliveDone then undo=>aliveNotDone; else had canUndo=false meaning
+    // !aliveDone, which can only be aliveNotDone given the state set). The second undo therefore
+    // cannot succeed — but the verifier must not let the first if's truth assertion leak.
+    public static void sequentialIfsLoseState() {
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        if (edit.canUndo()) {
+            edit.undo();
+        }
+        if (edit.canUndo()) {
+        }
+        edit.undo(); // State Refinement Error
+    }
+
+    // Wrong direction: canRedo() implies aliveNotDone, so calling undo() in that branch is illegal.
+    public static void undoGuardedByCanRedo(AbstractUndoableEdit edit) {
+        if (edit.canRedo()) {
+            edit.undo(); // State Refinement Error
+        }
+    }
+
+    // Redo after undo inside the then: the inner state is aliveDone -> aliveNotDone -> aliveDone
+    // after redo, so a second redo from aliveDone is illegal.
+    public static void doubleRedoAfterUndo(AbstractUndoableEdit edit) {
+        if (edit.canUndo()) {
+            edit.undo();
+            edit.redo();
+            edit.redo(); // State Refinement Error
+        }
+    }
+
+    // Empty if / empty else: the bug we fixed would have let `pathVar == true` (or false) leak past
+    // the join, masking violations. Here the constructor leaves edit in aliveDone, neither branch
+    // changes it, so after the if the state is still aliveDone — calling redo() is illegal.
+    public static void redoAfterEmptyIfElse() {
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        if (edit.canUndo()) {
+        } else {
+        }
+        edit.redo(); // State Refinement Error
+    }
+}