added unit tests for exclusive refinement.

1 files changed, 43 insertions, 0 deletions

diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy
new file mode 100644
index 00000000..bac08fba
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+include "Queue.dfyi"

+

+module LIFO exclusively refines Queue {

+    type Item = int

+

+    method Init() returns (q: Queue) {

+        q := [];

+    }

+

+    method Push(item: Item, q: Queue) returns (q': Queue) {

+        return [item] + q;

+    }

+

+    method Pop(q: Queue) returns (item: Item, q': Queue)

+        ensures item == q[0]

+    {

+        item := q[0];

+        q' := q[1..];

+    }

+}

+

+module MainImpl refines MainSpec {

+    import Q = LIFO

+

+    method Main()

+    {

+        var q := Q.Init();

+        q := Q.Push(0, q);

+        q := Q.Push(1, q);

+        q := Q.Push(2, q);

+

+        var n: int;

+        n, q := Q.Pop(q);

+        print n, "\n";

+        n, q := Q.Pop(q);

+        print n, "\n";

+        n, q := Q.Pop(q);

+        print n, "\n";

+    }

+}