From ddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 5 Nov 2009 01:24:43 +0000
Subject: 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.

---
 Test/dafny0/DTypes.dfy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Test/dafny0/DTypes.dfy')

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;
-- 
cgit v1.2.3