diff options
author | Rustan Leino <leino@microsoft.com> | 2011-08-04 02:10:36 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-08-04 02:10:36 -0700 |
commit | 13c53fb0caad70ba1a516285cae2587616217e2b (patch) | |
tree | 0fd4d67a8b0b88675f4de5056f1a52836bd1f797 | |
parent | f3c87e06dfa02a6c1300c5bef44d9d9218e1e2d5 (diff) |
Dafny: added reverse*reverse=id example to test suite
-rw-r--r-- | Test/dafny1/Answer | 2 | ||||
-rw-r--r-- | Test/dafny1/Rippling.dfy | 32 |
2 files changed, 33 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 5ee9f921..2b60b851 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -85,7 +85,7 @@ Dafny program verifier finished with 29 verified, 0 errors -------------------- Rippling.dfy --------------------
-Dafny program verifier finished with 132 verified, 0 errors
+Dafny program verifier finished with 137 verified, 0 errors
-------------------- Celebrity.dfy --------------------
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 0a4d541d..5fd87a6c 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -234,6 +234,13 @@ function sort(xs: List): List case Cons(y, ys) => insort(y, sort(ys))
}
+function reverse(xs: List): List
+{
+ match xs
+ case Nil => Nil
+ case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))
+}
+
// Pair list functions
function zip(a: List, b: List): PList
@@ -554,3 +561,28 @@ ghost method P67() assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
}
}
+
+// ---------
+
+ghost method Lemma_RevConcat(xs: List, ys: List)
+ ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ assert forall ws :: concat(ws, Nil) == ws;
+ case Cons(t, rest) =>
+ Lemma_RevConcat(rest, ys);
+ assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
+ }
+}
+
+ghost method Theorem(xs: List)
+ ensures reverse(reverse(xs)) == xs;
+{
+ match (xs) {
+ case Nil =>
+ case Cons(t, rest) =>
+ Lemma_RevConcat(reverse(rest), Cons(t, Nil));
+ Theorem(rest);
+ }
+}
|