From b5b29c378a82415e1d2b40528d06845f9c32d3ac Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 5 Jul 2011 18:22:41 -0700
Subject: Dafny: Updated regression tests to include chaining disjoint
 operators.

---
 Test/dafny0/Answer                    |  7 +++++--
 Test/dafny0/ChainingDisjointTests.dfy | 33 +++++++++++++++++++++++++++++++++
 Test/dafny0/ParseErrors.dfy           |  2 +-
 Test/dafny0/runtest.bat               |  2 +-
 4 files changed, 40 insertions(+), 4 deletions(-)
 create mode 100644 Test/dafny0/ChainingDisjointTests.dfy

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 384037ae..e5621773 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -450,12 +450,11 @@ ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
 ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator
 ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator
 ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator
-ParseErrors.dfy(14,18): error: this operator cannot be part of a chain
 ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
 ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
 ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
 ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-9 parse errors detected in ParseErrors.dfy
+8 parse errors detected in ParseErrors.dfy
 
 -------------------- Array.dfy --------------------
 Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -1100,3 +1099,7 @@ ReturnErrors.dfy(41,10): Error: can only have initialization methods which modif
 -------------------- ReturnTests.dfy --------------------
 
 Dafny program verifier finished with 16 verified, 0 errors
+
+-------------------- ChainingDisjointTests.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny0/ChainingDisjointTests.dfy b/Test/dafny0/ChainingDisjointTests.dfy
new file mode 100644
index 00000000..17a4fa9f
--- /dev/null
+++ b/Test/dafny0/ChainingDisjointTests.dfy
@@ -0,0 +1,33 @@
+
+method testing1() 
+{
+   var a, b, c := {1,2}, {3, 4}, {5, 6};
+   assert a !! b !! c;
+   testing2(a, b, c);
+   assert !({1,2} !! {2,3});
+   assert !({1,2} !! {9} !! {2,3}); // tests the accumulation
+   assert !({1,2} !! {9} !! {2,3});
+   assert !({1,2} !! {9} !! {8} !! {2,3}); // doesn't break at 4. that seems like a good stopping place.
+   assert !({9} !! {1,2} !! {8} !! {2,3});
+   assert !({9} !! {1} + {2} !! {8} !! {2,3}); // mixing in some other operators
+   assert !({1} !! {1} + {2});
+}
+
+method testing2(a: set<int>, b: set<int>, c: set<int>)
+   requires a !! b !! c;
+{
+   assert a !! b;
+   assert a !! c;
+   assert b !! c;
+}
+
+method testing3(a: set<int>, b: set<int>, c: set<int>, d: set<int>) // again with the four.
+   requires a !! b !! c !! d;
+{
+   assert a !! b;
+   assert a !! c;
+   assert b !! c;
+   assert a !! d;
+   assert b !! d;
+   assert c !! d;
+}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index d6f3005d..41df50eb 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -11,7 +11,7 @@ method TestChaining0(j: int, k: int, m: int)
 method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set<T>>)
   requires s <= t <= u >= s+u;  // error: cannot mix <= and >=
   ensures s <= u;
-  ensures s !! t !! u;  // error: !! is not chaining (but it would be nice if it were)
+  ensures s !! t !! u; // valid, means pairwise disjoint
   ensures x in s in SuperSet;  // error: 'in' is not chaining
   ensures x !in s in SuperSet;  // error: 'in' is not chaining
   ensures x in s !in SuperSet;  // error: 'in' is not chaining
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f606c183..143a0dc5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -19,7 +19,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Termination.dfy DTypes.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
-            ReturnErrors.dfy ReturnTests.dfy) do (
+            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 %* %%f
-- 
cgit v1.2.3