Added tests: parallel calc, better well-formedness checks, calc expression.

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;

+          }

+      }

+  }

+}

+