From 2cca81470c1b536a4bdea3f2f727e00fcfa702c6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sat, 2 Feb 2013 10:43:30 -0800
Subject: Added some test cases that show exmaples that iterate over set
 elements.

---
 Test/dafny3/Answer            |  4 +++
 Test/dafny3/SetIterations.dfy | 72 +++++++++++++++++++++++++++++++++++++++++++
 Test/dafny3/runtest.bat       |  2 +-
 3 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny3/SetIterations.dfy

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 8812f389..284c5233 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -34,3 +34,7 @@ Dafny program verifier finished with 20 verified, 0 errors
 -------------------- Zip.dfy --------------------
 
 Dafny program verifier finished with 24 verified, 0 errors
+
+-------------------- SetIterations.dfy --------------------
+
+Dafny program verifier finished with 13 verified, 0 errors
diff --git a/Test/dafny3/SetIterations.dfy b/Test/dafny3/SetIterations.dfy
new file mode 100644
index 00000000..8b095b5f
--- /dev/null
+++ b/Test/dafny3/SetIterations.dfy
@@ -0,0 +1,72 @@
+function Count<T>(s: set<T>): int
+{
+  if s == {} then 0 else
+    var x :| x in s;  // let x be such that "x in s"
+    1 + Count(s - {x})
+}
+
+method Copy<T>(s: set<T>) returns (t: set<T>)
+  ensures s == t;
+{
+  t := {};
+  var r := s;
+  while (r != {})
+    invariant s == r + t;
+    decreases r;
+  {
+    var x :| x in r;
+    r, t := r - {x}, t + {x};
+  }
+}
+
+method CopyFaster<T>(s: set<T>) returns (t: set<T>)
+  ensures s == t;
+{
+  t := {};
+  var r := s;
+  while (r != {})
+    invariant s == r + t;
+    decreases r;
+  {
+    var p :| p != {} && p <= r;  // pick a nonempty subset of r
+    r, t := r - p, t + p;
+  }
+}
+
+method CopyFastest<T>(s: set<T>) returns (t: set<T>)
+  ensures s == t;
+{
+  t := s;  // :)
+}
+
+iterator Iter<T>(s: set<T>) yields (x: T)
+  yield ensures x in s && x !in xs[..|xs|-1];
+  ensures s == set z | z in xs;
+{
+  var r := s;
+  while (r != {})
+    invariant forall z :: z in xs ==> x !in r;  // r and xs are disjoint
+    invariant s == r + set z | z in xs;
+  {
+    var y :| y in r;
+    r, x := r - {y}, y;
+    yield;
+    assert y == xs[|xs|-1];  // needed as a lemma to prove loop invariant
+  }
+}
+
+method UseIterToCopy<T>(s: set<T>) returns (t: set<T>)
+  ensures s == t;
+{
+  t := {};
+  var m := new Iter(s);
+  while (true)
+    invariant m.Valid() && fresh(m._new);
+    invariant t == set z | z in m.xs;
+    decreases s - t;
+  {
+    var more := m.MoveNext();
+    if (!more) { break; }
+    t := t + {m.x};
+  }
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index aeffee89..82fd878c 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -7,7 +7,7 @@ set DAFNY_EXE=%BINARIES%\Dafny.exe
 for %%f in (
   Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy
   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy
-  InductionVsCoinduction.dfy Zip.dfy
+  InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy
 ) do (
   echo.
   echo -------------------- %%f --------------------
-- 
cgit v1.2.3