1 files changed, 22 insertions, 0 deletions
diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi
new file mode 100644
index 00000000..06f4b29e
--- /dev/null
+++ b/Test/irondafny0/Queue.dfyi
@@ -0,0 +1,22 @@
+// Queue.dfyi
+
+abstract module Queue {
+    type Item
+    type Queue = seq<Item>
+
+    method Init() returns (q: Queue)
+        ensures |q| == 0;
+
+    method Push(item: Item, q: Queue) returns (q': Queue)
+        ensures |q'| == |q| + 1;
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        requires |q| > 0;
+        ensures item in q;
+        ensures |q'| == |q| - 1;
+}
+
+abstract module MainSpec {
+    import Q : Queue
+}
+