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.

1 files changed, 6 insertions, 6 deletions

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 ==>