diff options
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/SetIterations.dfy | 72 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 2 |
3 files changed, 77 insertions, 1 deletions
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 --------------------
|