Dafny: Updated regression tests to include chaining disjoint operators.

4 files changed, 40 insertions, 4 deletions

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