Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)".

Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.

6 files changed, 30 insertions, 25 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 0149855c..a9fd2367 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -26,3 +26,7 @@ Dafny program verifier finished with 12 verified, 0 errors
 -------------------- b7.dfy --------------------

 

 Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- b8.dfy --------------------

+

+Dafny program verifier finished with 21 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b0b370a0..ac58b7d1 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -26,7 +26,7 @@ class Map<Key,Value> {
 

   method Find(key: Key) returns (present: bool, val: Value)

     requires Valid();

-    ensures !present ==> !(key in keys);

+    ensures !present ==> key !in keys;

     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

@@ -78,9 +78,9 @@ class Map<Key,Value> {
     ensures (forall k :: k in old(keys) ==> k in keys || k == key);

     // the given key is not there:

     // other values don't change:

-    ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);

+    ensures key !in old(keys) ==> keys == old(keys) && values == old(values);

     ensures key in old(keys) ==>

-            !(key in keys) &&

+            key !in keys &&

             (exists h ::

               0 <= h && h <= |keys| &&

               keys[..h] == old(keys)[..h] &&

@@ -99,13 +99,13 @@ class Map<Key,Value> {
   method FindIndex(key: Key) returns (idx: int)

     requires Valid();

     ensures -1 <= idx && idx < |keys|;

-    ensures idx == -1 ==> !(key in keys);

+    ensures idx == -1 ==> key !in keys;

     ensures 0 <= idx ==> keys[idx] == key;

   {

     var j := 0;

     while (j < |keys|)

       invariant j <= |keys|;

-      invariant !(key in keys[..j]);

+      invariant key !in keys[..j];

       decreases |keys| -j;

     {

       if (keys[j] == key) {

diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy
index e5d061d2..f6e7879f 100644
--- a/Test/VSI-Benchmarks/b6.dfy
+++ b/Test/VSI-Benchmarks/b6.dfy
@@ -63,7 +63,7 @@ class Iterator {
   function Valid():bool

   reads this, footprint;

   {

-		this in footprint && c!= null && -1<= pos && !(null in footprint)

+		this in footprint && c!= null && -1<= pos && null !in footprint

   }

   

   method Init(coll:Collection)

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 13a8ccd2..95267823 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -36,7 +36,7 @@ class Stream {
   function Valid():bool

   reads this, footprint;

   {

-	!(null in footprint) && this in footprint && isOpen

+	null !in footprint && this in footprint && isOpen

   }

   

   method GetCount() returns (c:int)

@@ -152,7 +152,7 @@ class Client {
 	    var wr:= new Stream;

 	    call wr.Create();

 	    while (0<|q.contents|)

-	    invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);

+	    invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;

 	    decreases |q.contents|;

 		{

 				call ch:= q.Dequeue();	

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index d499d017..643609d0 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -54,10 +54,10 @@ class Glossary {
     while (true)

       invariant rs.Valid() && fresh(rs.footprint);

       invariant glossary.Valid();

-      invariant !(glossary in rs.footprint);

-      invariant !(null in glossary.keys);

+      invariant glossary !in rs.footprint;

+      invariant null !in glossary.keys;

       //to do add invariant  invariant (forall d:: d in glossary.values ==>!(null in d)); ***

-      invariant !(q in rs.footprint);

+      invariant q !in rs.footprint;

       //  ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end)

       // we leave out the decreases clause - unbounded stream

     {

@@ -80,8 +80,8 @@ class Glossary {
     while (0<|q.contents|)

       invariant wr.Valid() && fresh(wr.footprint);

       invariant glossary.Valid();

-      invariant !(glossary in wr.footprint) && !(null in glossary.keys);

-      invariant !(q in wr.footprint);

+      invariant glossary !in wr.footprint && null !in glossary.keys;

+      invariant q !in wr.footprint;

       decreases |q.contents|;

     {

       var term, present, definition;

@@ -97,8 +97,8 @@ class Glossary {
       while (i < |definition|)

         invariant wr.Valid() && fresh(wr.footprint);

         invariant glossary.Valid();

-        invariant !(glossary in wr.footprint) && !(null in glossary.keys);

-        invariant !(q in wr.footprint); 

+        invariant glossary !in wr.footprint && null !in glossary.keys;

+        invariant q !in wr.footprint;

         invariant qcon == q.contents;

         decreases |definition| -i;

       {

@@ -125,7 +125,7 @@ class Glossary {
     requires rs != null && rs.Valid();

     modifies rs.footprint;

     ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint));

-    ensures term != null ==> !(null in definition);

+    ensures term != null ==> null !in definition;

   {

     call term := rs.GetWord();

     if (term != null)

@@ -133,7 +133,7 @@ class Glossary {
       definition := [];

       while (true)

         invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint));

-        invariant !(null in definition);

+        invariant null !in definition;

       {

         var w;

         call w := rs.GetWord();

@@ -159,7 +159,7 @@ class ReaderStream {
   function Valid():bool

   reads this, footprint;

   {

-    !(null in footprint) && this in footprint && isOpen

+    null !in footprint && this in footprint && isOpen

   }

   

   method Open() //reading

@@ -193,7 +193,7 @@ class WriterStream {
   function Valid():bool

   reads this, footprint;

   {

-    !(null in footprint) && this in footprint && isOpen

+    null !in footprint && this in footprint && isOpen

   }

   

   method Create() //writing

@@ -271,7 +271,7 @@ class Map<Key,Value> {
 

   method Find(key: Key) returns (present: bool, val: Value)

     requires Valid();

-    ensures !present ==> !(key in keys);

+    ensures !present ==> key !in keys;

     ensures present ==> (exists i :: 0 <= i && i < |keys| &&

                                      keys[i] == key && values[i] == val);

   {

@@ -323,9 +323,9 @@ class Map<Key,Value> {
     ensures (forall k :: k in old(keys) ==> k in keys || k == key);

     // the given key is not there:

     // other values don't change:

-    ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values);

+    ensures key !in old(keys) ==> keys == old(keys) && values == old(values);

     ensures key in old(keys) ==>

-            !(key in keys) &&

+            key !in keys &&

             (exists h ::

               0 <= h && h <= |keys| &&

               keys[..h] == old(keys)[..h] &&

@@ -344,13 +344,13 @@ class Map<Key,Value> {
   method FindIndex(key: Key) returns (idx: int)

     requires Valid();

     ensures -1 <= idx && idx < |keys|;

-    ensures idx == -1 ==> !(key in keys);

+    ensures idx == -1 ==> key !in keys;

     ensures 0 <= idx ==> keys[idx] == key;

   {

     var j := 0;

     while (j < |keys|)

       invariant j <= |keys|;

-      invariant !(key in keys[..j]);

+      invariant key !in keys[..j];

       decreases |keys| -j;

     {

       if (keys[j] == key) {

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a8658aef..fa737dca 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -7,7 +7,8 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
 

 

 

-for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy) do (

+for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy

+             b8.dfy ) do (

   echo.

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

   %DAFNY_EXE% %* %%f