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/dafny0/Answer           |  6 ++--
 Test/dafny0/Calculations.dfy | 16 +++++++++++
 Test/dafny2/Answer           |  2 +-
 Test/dafny2/Calculations.dfy | 65 +++++++++++++++++++++++++++++++++++++++++++-
 4 files changed, 84 insertions(+), 5 deletions(-)

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a5c48e9a..c738f058 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1795,12 +1795,12 @@ Calculations.dfy(8,17): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon13_Then
-Calculations.dfy(36,11): Error: assertion violation
+Calculations.dfy(42,11): Error: assertion violation
 Execution trace:
     (0,0): anon0
-    Calculations.dfy(31,2): anon5_Else
+    Calculations.dfy(37,2): anon5_Else
 
-Dafny program verifier finished with 4 verified, 4 errors
+Dafny program verifier finished with 5 verified, 4 errors
 
 -------------------- IteratorResolution.dfy --------------------
 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 80775896..aa447d9f 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -16,6 +16,12 @@ method CalcTest0(s: seq<int>) {
 			s[0];
 		}
 	}
+	assume forall x :: x in s ==> x >= 0;
+	calc ==> {
+		0 < |s|;
+		{ assert s[0] >= 0; } // OK: well-formed after previous line
+		s[0] >= 0; // OK: well-formed after previous line
+	}
 }
 
 method CalcTest1(x: int, y: int) {
@@ -34,4 +40,14 @@ method CalcTest2(x: int, y: int) {
 		y + x;
 	}
 	assert x == 0; // error: even though assumed above, is not exported by the calculation
+}
+
+// calc expression:
+function CalcTest(s: seq<int>): int {
+	calc < {
+		0;
+		{ assume |s| == 5; }
+		|s|;
+	}
+	s[0]
 }
\ No newline at end of file
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