Iterator example

part4/exercises-add-refinements/src/Iterator.java

@@ -0,0 +1,19 @@
+import repair.regen.specification.StateRefinement;
+import repair.regen.specification.StateSet;
+
+@StateSet({"notready", "ready", "finished"})
+public class Iterator {
+	boolean hn;
+
+	@StateRefinement(from = "notready(this)", to = "ready(this)")
+	boolean hasNext(boolean hn) { return hn; }
+
+	@StateRefinement(from = "ready(this)", to = "finished(this)")
+	int next(boolean hn) { 
+		if (hn) {
+			return 1;
+		} else {
+			return -1;
+		}
+	}
+}

part4/exercises-add-refinements/src/IteratorWrong.java

@@ -0,0 +1,9 @@
+public class IteratorWrong {
+	public static void main() {
+		Iterator i = new Iterator(); // i -> "notready"
+		boolean hn = true;
+		// i.next() requires state "ready" but i is "notready"
+		int x = i.next(hn); // shouldn't be accepted by the typechecker ;-;
+	}
+}
+