From c82aa24e26e14c4f58df4bd77afc9b82464f7a83 Mon Sep 17 00:00:00 2001
From: Lisa Vasilenko <vasilliza@gmail.com>
Date: Mon, 19 Sep 2022 16:34:08 +0100
Subject: [PATCH] iterator

---
 .../src/Iterator.java                         | 19 +++++++++++++++++++
 .../src/IteratorWrong.java                    |  9 +++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 part4/exercises-add-refinements/src/Iterator.java
 create mode 100644 part4/exercises-add-refinements/src/IteratorWrong.java

diff --git a/part4/exercises-add-refinements/src/Iterator.java b/part4/exercises-add-refinements/src/Iterator.java
new file mode 100644
index 0000000..e4ecf0a
--- /dev/null
+++ b/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;
+		}
+	}
+}
\ No newline at end of file
diff --git a/part4/exercises-add-refinements/src/IteratorWrong.java b/part4/exercises-add-refinements/src/IteratorWrong.java
new file mode 100644
index 0000000..c183124
--- /dev/null
+++ b/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 ;-;
+	}
+}
+