Dafny: Added maps to regression tests.

4 files changed, 203 insertions, 2 deletions

diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy
new file mode 100644
index 00000000..eb543283
--- /dev/null
+++ b/Test/dafny0/Maps.dfy
@@ -0,0 +1,141 @@
+

+// This method can be used to test compilation.

+method Main()

+{

+   var m:= map{2:=3};

+   // test "in"

+   if(2 in m)

+   {

+      print "m0\n";

+   }

+   else

+   { assert false; }

+   // test "!in"

+   if(3 !in m)

+   {

+      print "m1\n";

+   }

+   else

+   { assert false; }

+   // dereference

+   if(m[2] == 3)

+   {

+      print "m2\n";

+   }

+   else

+   { assert false; }

+   // test disjoint operator

+   if(m !! map{3 := 3})

+   {

+      print "m3\n";

+   }

+   else

+   { assert false; }

+   // updates should replace values that already exist

+   if(m[2 := 4] == map{2 := 4})

+   {

+      print "m4\n";

+   }

+   else

+   { assert false; }

+   // add something to the map

+   if(m[7 := 1] == map{2 := 3,7 := 1})

+   {

+      print "m5\n";

+   }

+   else

+   { assert false; }

+   // test applicative nature of Map<U, V> in C#

+   if(m == map{2 := 3})

+   {

+      print "m6\n";

+   }

+   else

+   { assert false; }

+   // this should print all m1, m2, ... m6.

+}

+

+method m()

+{

+   var a := map{2:=3}; var b := map{3:=2};

+   assert a[b[3]] == 3;

+}

+method m2(a: map<int, bool>, b: map<int, bool>)

+   requires forall i | 0 <= i < 100 :: i in a && i in b && a[i] != b[i];

+{

+   assert forall i | 0 <= i < 100 :: a[i] || b[i];

+}

+method m3(a: map<int, int>)

+   requires forall i | 0 <= i < 100 :: i in a && a[i] == i*i;

+{

+   assert a[20] == 400;

+}

+method m4()

+{

+   var a := map{3 := 9};

+   if(a[4] == 4) // UNSAFE, 4 not in the domain

+   {

+      m();

+   }

+}

+

+method m5(a: map<int, int>)

+   requires 20 in a;

+{

+   assert a[20] <= 0 || 0 < a[20];

+}

+method m6()

+{

+   var a := map{3 := 9};

+   assert a[3:=5] == map{3:=5};

+   assert a[2:=5] == map{2:=5, 3:=9};

+   assert a[2:=5] == map{2:=6, 3:=9, 2:=5}; // test the ordering of assignments in the map literal

+}

+method m7()

+{

+   var a := map{1:=1, 2:=4, 3:=9};

+   assert forall i | i in a :: a[i] == i * i;

+   assert 0 !in a;

+   assert 1 in a;

+   assert 2 in a;

+   assert 3 in a;

+   assert forall i | i < 1 || i > 3 :: i !in a;

+}

+method m8()

+{

+   var a := map{};

+   assert forall i :: i !in a; // check emptiness

+   var i,n := 0, 100;

+   while(i < n)

+      invariant 0 <= i <= n;

+      invariant forall i | i in a :: a[i] == i * i;

+	  invariant forall k :: 0 <= k < i <==> k in a;

+   {

+      a := a[i := i * i];

+      i := i + 1;

+   }

+   assert a !! map{-1:=2};

+   m3(a);

+}

+method m9()

+{

+   var a, b := map{}, map{};

+   assert a !! b;

+   b := map{2:=3,4:=2,5:=-6,6:=7};

+   assert a !! b;

+   assert b !! map{6:=3}; // ERROR, both share 6 in the domain.

+}

+method m10()

+{

+   var a, b := map{}, map{};

+   assert a !! b;

+   b := map{2:=3,4:=2,5:=-6,6:=7};

+   assert a !! b;

+   a := map{3:=3,1:=2,9:=-6,8:=7};

+   assert a !! b;

+}

+method m11<U, V>(a: map<U, V>, b: map<U, V>)

+   requires forall i :: !(i in a && i in b);

+{

+   assert a !! b;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index fa81bb8c..e4c134f6 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -22,7 +22,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

-            Predicates.dfy Skeletons.dfy) do (

+            Predicates.dfy Skeletons.dfy Maps.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
new file mode 100644
index 00000000..3b6e478c
--- /dev/null
+++ b/Test/dafny1/BDD.dfy
@@ -0,0 +1,60 @@
+

+

+module SimpleBDD

+{

+   class BDDNode

+   {

+     static predicate bitfunc(f: map<seq<bool>, bool>, n: nat)

+	 {

+	    forall i:seq<bool> :: i in f <==> |i| == n

+	 }

+      ghost var Contents: map<seq<bool>, bool>;

+	  ghost var Repr: set<object>;

+	  ghost var n: nat;

+	  var f: BDDNode, t: BDDNode;

+	  var b: bool;

+	  predicate valid()

+	    reads this, Repr;

+	  {

+	    bitfunc(Contents,n) &&

+		(0 == n ==> (b <==> Contents[[]])) &&

+		(0 < n ==> this in Repr && f != null && t != null && t in Repr && f in Repr && t.Repr <= Repr && f.Repr <= Repr && this !in f.Repr && this !in t.Repr && t.valid() && f.valid() &&

+		 t.n == f.n == n-1 &&

+		 (forall s | s in t.Contents :: Contents[[true]  + s] <==> t.Contents[s]) &&

+		 (forall s | s in f.Contents :: Contents[[false] + s] <==> f.Contents[s]))

+	  }

+   }

+   class BDD

+   {

+     var root: BDDNode;

+	 predicate valid()

+	   reads this, Repr;

+	 {

+	   root != null && root in Repr && root.Repr <= Repr && root.valid() && 

+	   n == root.n && Contents == root.Contents

+	 }

+

+     ghost var Contents: map<seq<bool>, bool>;

+	 var n: nat;

+	 ghost var Repr: set<object>;

+

+	 method Eval(s: seq<bool>) returns(b: bool)

+	    requires valid() && |s| == n;

+		ensures b == Contents[s];

+	 {

+	   var node: BDDNode := root;

+	   var i := n;

+	   assert s[n-i..] == s;

+	   while(i > 0)

+	     invariant node != null && node.valid();

+	     invariant 0 <= i == node.n <= n;

+		 invariant Contents[s] == node.Contents[s[n-i..]];

+	   {

+	     assert s[n-i..] == [s[n-i]] + s[n-i+1..];

+		 node := if s[n-i] then node.t else node.f;

+		 i := i - 1;

+	   }

+	   b := node.b;

+	 }

+   }

+}
\ No newline at end of file
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 0ad75ffa..1f5d78df 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -23,7 +23,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy
             Cubes.dfy SumOfCubes.dfy FindZero.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

             Induction.dfy Rippling.dfy MoreInduction.dfy

-            Celebrity.dfy

+            Celebrity.dfy BDD.dfy

             UltraFilter.dfy) do (

   echo.

   echo -------------------- %%f --------------------