summaryrefslogtreecommitdiff
path: root/Test/dafny3/SetIterations.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny3/SetIterations.dfy')
-rw-r--r--Test/dafny3/SetIterations.dfy72
1 files changed, 72 insertions, 0 deletions
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};
+ }
+}