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.

11 files changed, 46 insertions, 41 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

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index b3bcc823..7a5fb3c7 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -12,7 +12,7 @@ class IntSet {
     (root != null ==>

        root in footprint && root.Valid() &&

        contents == root.contents &&

-       root.footprint <= footprint && !(this in root.footprint))

+       root.footprint <= footprint && this !in root.footprint)

   }

 

   method Init()

@@ -112,14 +112,14 @@ class Node {
     reads this, footprint;

   {

     this in footprint &&

-    !(null in footprint) &&

+    null !in footprint &&

     (left != null ==>

       left in footprint && left.Valid() &&

-      left.footprint <= footprint && !(this in left.footprint) &&

+      left.footprint <= footprint && this !in left.footprint &&

       (forall y :: y in left.contents ==> y < data)) &&

     (right != null ==>

       right in footprint && right.Valid() &&

-      right.footprint <= footprint && !(this in right.footprint) &&

+      right.footprint <= footprint && this !in right.footprint &&

       (forall y :: y in right.contents ==> data < y)) &&

     (left == null && right == null ==>

       contents == {data}) &&

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index f6e0a2b4..c468cff4 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -5,14 +5,14 @@ class C {
     requires v != null;

   {

     var o: object := v;

-    assert !(o in n);  // should be known from the types involved

+    assert o !in n;  // should be known from the types involved

   }

 

   method N(v: Stack)

     /* this time without the precondition */

   {

     var o: object := v;

-    assert !(o in n);  // error: v may be null

+    assert o !in n;  // error: v may be null

   }

 

   method A0(a: CP<int,C>, b: CP<int,object>)

@@ -31,7 +31,7 @@ class C {
 

   var a2x: set<CP<C,Node>>;

   method A2(b: set<CP<Node,C>>)

-    requires !(null in b);

+    requires null !in b;

   {

     var x: set<object> := a2x;

     var y: set<object> := b;

diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
index 6cb7c5a0..01d8b63b 100644
--- a/Test/dafny0/ListContents.dfy
+++ b/Test/dafny0/ListContents.dfy
@@ -8,11 +8,11 @@ class Node<T> {
   function Valid(): bool

     reads this, footprint;

   {

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

+    this in this.footprint && null !in this.footprint &&

     (next == null ==> list == [data]) &&

     (next != null ==>

         next in footprint && next.footprint <= footprint &&

-        !(this in next.footprint) &&

+        this !in next.footprint &&

         list == [data] + next.list &&

         next.Valid())

   }

diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy
index af61a7a3..08b14751 100644
--- a/Test/dafny0/ListReverse.dfy
+++ b/Test/dafny0/ListReverse.dfy
@@ -3,7 +3,7 @@ class Node {
   var nxt: Node;

 

   method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)

-    requires !(null in r);

+    requires null !in r;

     requires x == null || x in r;

     requires (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure

     modifies r;

diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy
index db5928f4..20db882a 100644
--- a/Test/dafny0/SchorrWaite.dfy
+++ b/Test/dafny0/SchorrWaite.dfy
@@ -92,7 +92,7 @@ class Main {
     var stackNodes := [];

     var unmarkedNodes := S - {t};  // used as ghost variable

     while (true)

-      invariant root.marked && t in S && !(t in stackNodes);

+      invariant root.marked && t in S && t !in stackNodes;

       // stackNodes has no duplicates:

       invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>

                   stackNodes[i] != stackNodes[j]);

@@ -108,9 +108,9 @@ class Main {
                   stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]);

       invariant 0 < |stackNodes| ==>

         stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;

-      invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>

+      invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>

                   (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

-      invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>

+      invariant (forall n :: n in S && n !in stackNodes && n != t ==>

                 n.childrenVisited == old(n.childrenVisited));

       invariant (forall n: Node :: n.children == old(n.children));

       invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);

@@ -161,7 +161,7 @@ class Main {
     var stackNodes := [];  // used as ghost variable

     var unmarkedNodes := S - {t};  // used as ghost variable

     while (true)

-      invariant root.marked && t != null && t in S && !(t in stackNodes);

+      invariant root.marked && t != null && t in S && t !in stackNodes;

       invariant |stackNodes| == 0 <==> p == null;

       invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1];

       // stackNodes has no duplicates:

@@ -174,9 +174,9 @@ class Main {
                   (forall j :: 0 <= j && j < n.childrenVisited ==>

                     n.children[j] == null || n.children[j].marked));

       invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);

-      invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>

+      invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>

                   (forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));

-      invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>

+      invariant (forall n :: n in S && n !in stackNodes && n != t ==>

                 n.childrenVisited == old(n.childrenVisited));

       invariant (forall n :: n in stackNodes || n.children == old(n.children));

       invariant (forall n :: n in stackNodes ==>