From 5c5d0318c70d53eb8b287b07edfce96b6888a540 Mon Sep 17 00:00:00 2001
From: Nadia Polikarpova <nadia.polikarpova@gmail.com>
Date: Fri, 15 Feb 2013 17:07:57 -0800
Subject: Added tests: parallel calc, better well-formedness checks, calc
 expression.

---
 Test/dafny2/Answer           |  2 +-
 Test/dafny2/Calculations.dfy | 65 +++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 65 insertions(+), 2 deletions(-)

(limited to 'Test/dafny2')

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index d83c766c..8e1ef967 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -57,4 +57,4 @@ Dafny program verifier finished with 36 verified, 0 errors
 
 -------------------- Calculations.dfy --------------------
 
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 31 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index c637147a..79803f35 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -207,4 +207,67 @@ ghost method Window(xs: List, ys: List)
     length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
     true;
   }
-}
\ No newline at end of file
+}
+
+// In the following we use a combination of calc and parallel
+
+function ith<a>(xs: List, i: nat): a
+  requires i < length(xs);
+{
+  match xs
+  case Cons(x, xrest) => if i == 0 then x else ith(xrest, i - 1)
+}
+
+ghost method lemma_zero_length(xs: List)
+  ensures length(xs) == 0 <==> xs.Nil?;
+{}
+
+ghost method lemma_extensionality(xs: List, ys: List)
+  requires length(xs) == length(ys); // (0)
+  requires forall i: nat | i < length(xs) :: ith(xs, i) == ith(ys, i); // (1)
+  ensures xs == ys;
+{
+  match xs {
+    case Nil => 
+      calc {
+        true;
+        // (0)
+        length(xs) == length(ys);
+        0 == length(ys);
+        { lemma_zero_length(ys); }
+        Nil == ys;
+        xs == ys;
+      }
+    case Cons(x, xrest) =>
+      match ys {
+        case Cons(y, yrest) =>
+          calc {
+            xs;
+            Cons(x, xrest);
+            calc {
+              x;
+              ith(xs, 0);
+              // (1) with i = 0
+              ith(ys, 0);
+              y;
+            }
+            Cons(y, xrest);
+            { 
+              parallel (j: nat | j < length(xrest)) {
+                calc {
+                  ith(xrest, j);
+                  ith(xs, j + 1);
+                  // (1) with i = j + 1
+                  ith(ys, j + 1);
+                  ith(yrest, j);
+                }
+              }
+              lemma_extensionality(xrest, yrest); 
+            }
+            Cons(y, yrest);
+            ys;
+          }
+      }
+  }
+}
+
-- 
cgit v1.2.3