Dafny: some test cases for "calc" (very cool!)

3 files changed, 217 insertions, 1 deletions

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index 447f4365..2feaf6f7 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -54,3 +54,7 @@ Dafny program verifier finished with 3 verified, 0 errors
 -------------------- MonotonicHeapstate.dfy --------------------

 

 Dafny program verifier finished with 36 verified, 0 errors

+

+-------------------- Calculations.dfy --------------------

+

+Dafny program verifier finished with 26 verified, 0 errors

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
new file mode 100644
index 00000000..8e3a4426
--- /dev/null
+++ b/Test/dafny2/Calculations.dfy
@@ -0,0 +1,212 @@
+/* Lists */

+// Here are some standard definitions of List and functions on Lists

+

+datatype List<T> = Nil | Cons(T, List);

+

+function length(l: List): nat

+{

+  match l

+  case Nil => 0

+  case Cons(x, xs) => 1 + length(xs)

+}

+

+function concat(l: List, ys: List): List

+{

+  match l

+  case Nil => ys

+  case Cons(x, xs) => Cons(x, concat(xs, ys))

+}

+

+function reverse(l: List): List

+{

+  match l

+  case Nil => Nil

+  case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))

+}

+

+function revacc(l: List, acc: List): List

+{

+  match l

+  case Nil => acc

+  case Cons(x, xs) => revacc(xs, Cons(x, acc))

+}

+

+function qreverse(l: List): List

+{

+  revacc(l, Nil)

+}

+

+// Here are two lemmas about the List functions.

+

+ghost method Lemma_ConcatNil()

+  ensures forall xs :: concat(xs, Nil) == xs;

+{

+}

+

+ghost method Lemma_RevCatCommute()

+  ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);

+{

+}

+

+// Here is a theorem that says "qreverse" and "reverse" calculate the same result.  The proof

+// is given in a calculational style.  The proof is not minimal--some lines can be omitted

+// and Dafny will still fill in the details.

+

+ghost method Theorem_QReverseIsCorrect_Calc(l: List)

+  ensures qreverse(l) == reverse(l);

+{

+  calc {

+    qreverse(l);

+    // def. qreverse

+    revacc(l, Nil);

+    { Lemma_Revacc_calc(l, Nil); }

+    concat(reverse(l), Nil);

+    { Lemma_ConcatNil(); }

+    reverse(l);

+  }

+}

+

+ghost method Lemma_Revacc_calc(xs: List, ys: List)

+  ensures revacc(xs, ys) == concat(reverse(xs), ys);

+{

+  match (xs) {

+    case Nil =>

+    case Cons(x, xrest) =>

+      calc {

+        concat(reverse(xs), ys);

+        // def. reverse

+        concat(concat(reverse(xrest), Cons(x, Nil)), ys);

+        // induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))

+        concat(revacc(xrest, Cons(x, Nil)), ys);

+        { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

+        revacc(xrest, concat(Cons(x, Nil), ys));

+        { 

+          assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs); 

+          assert concat(Cons(x, Nil), ys) == Cons(x, ys);

+        }

+        revacc(xrest, Cons(x, ys));

+        // def. revacc

+        revacc(xs, ys);

+      }

+  }

+}

+

+// Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.

+

+ghost method Theorem_QReverseIsCorrect(l: List)

+  ensures qreverse(l) == reverse(l);

+{

+  assert qreverse(l)

+      == // def. qreverse

+         revacc(l, Nil);

+  Lemma_Revacc(l, Nil);

+  assert revacc(l, Nil)

+      == concat(reverse(l), Nil);

+  Lemma_ConcatNil();

+}

+

+ghost method Lemma_Revacc(xs: List, ys: List)

+  ensures revacc(xs, ys) == concat(reverse(xs), ys);

+{

+  match (xs) {

+    case Nil =>

+    case Cons(x, xrest) =>

+      assert revacc(xs, ys)

+          == // def. revacc

+              revacc(xrest, Cons(x, ys));

+

+      assert concat(reverse(xs), ys)

+          == // def. reverse

+              concat(concat(reverse(xrest), Cons(x, Nil)), ys)

+          == // induction hypothesis:  Lemma3a(xrest, Cons(x, Nil))

+              concat(revacc(xrest, Cons(x, Nil)), ys);

+          Lemma_RevCatCommute();  // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

+      assert concat(revacc(xrest, Cons(x, Nil)), ys)

+          == revacc(xrest, concat(Cons(x, Nil), ys));

+

+      assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);

+

+      assert revacc(xrest, concat(Cons(x, Nil), ys))

+          == // the assert lemma just above

+              revacc(xrest, Cons(x, ys));

+  }

+}

+

+/* Fibonacci */

+// To further demonstrate what the "calc" construct can do, here are some proofs about the Fibonacci function.

+

+function Fib(n: nat): nat

+{

+  if n < 2 then n else Fib(n - 2) + Fib(n - 1)

+}

+

+ghost method Lemma_Fib()

+  ensures Fib(5) < 6;

+{

+  calc {

+    Fib(5);

+    Fib(4) + Fib(3);

+    calc {

+      Fib(2);

+      Fib(0) + Fib(1);

+      0 + 1;

+      1;

+    }

+    < 6;

+  }

+}

+

+/* List length */

+// Here are some proofs that show the use of nested calculations.

+

+ghost method Lemma_Concat_Length(xs: List, ys: List)

+  ensures length(concat(xs, ys)) == length(xs) + length(ys);

+{}

+

+ghost method Lemma_Reverse_Length(xs: List)

+  ensures length(xs) == length(reverse(xs));

+{

+  match (xs) {

+    case Nil =>

+    case Cons(x, xrest) =>

+      calc {

+        length(reverse(xs));

+        // def. reverse

+        length(concat(reverse(xrest), Cons(x, Nil)));

+        { Lemma_Concat_Length(reverse(xrest), Cons(x, Nil)); }

+        length(reverse(xrest)) + length(Cons(x, Nil));

+        // induction hypothesis

+        length(xrest) + length(Cons(x, Nil));

+        calc {

+          length(Cons(x, Nil));

+          // def. length

+          1 + length(Nil);

+          // def. length

+          1 + 0;

+          1;

+        }

+        length(xrest) + 1;

+        // def. length

+        length(xs);

+      }

+  }

+}

+

+ghost method Window(xs: List, ys: List)

+  ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));

+{

+  calc {

+    length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));

+    { if (length(xs) == length(ys)) {

+      calc {

+        length(reverse(xs));

+        { Lemma_Reverse_Length(xs); }

+        length(xs);

+        length(ys);

+        { Lemma_Reverse_Length(ys); }

+        length(reverse(ys));

+    } } }

+    length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));

+    true;

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 909f67f5..72959830 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (
     StoreAndRetrieve.dfy

     Intervals.dfy TreeFill.dfy TuringFactorial.dfy

     MajorityVote.dfy SegmentSum.dfy

-    MonotonicHeapstate.dfy

+    MonotonicHeapstate.dfy Calculations.dfy

   ) do (

   echo.

   echo -------------------- %%f --------------------