1 files changed, 0 insertions, 59 deletions
diff --git a/Chalice/tests/examples/UnboundedThreads.chalice b/Chalice/tests/examples/UnboundedThreads.chalice
deleted file mode 100644
index c52bb10a..00000000
--- a/Chalice/tests/examples/UnboundedThreads.chalice
+++ /dev/null
@@ -1,59 +0,0 @@
-class C {
-  
-  var f: int;
-  
-  method main(n: int)
-    requires n > 0 && acc(this.f)
-    ensures acc(this.f)
-  {
-    // fork all threads, and join them afterwards
-    call work(n);
-    
-    this.f := 100; // we want a full permission in the end
-  }
-
-  method work(n: int)
-    requires rd(this.f,n)
-    ensures rd(this.f,n)
-  {
-    var tks:seq<token<C.m>> := nil<token<C.m>>;
-    
-    // first loop; fork all threads
-    var i := 0;
-    while (i < n)
-      invariant i <= n && |tks| == i;
-      invariant i < n ==> rd(this.f,n-i);
-      invariant acc(tks[*].joinable);
-      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
-      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
-      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
-    {
-      fork tk := m();
-      tks := tks ++ [tk];
-      i := i+1;
-    }
-    
-    // second loop; join all threads
-    i := n;
-    while (i > 0)
-      invariant i >= 0 && |tks| == i;
-      invariant i < n ==> rd(this.f,n-i); // BUG: the eval construct inside the quantification does not give us the information needed to proof this invariant, see http://boogie.codeplex.com/workitem/10187
-      invariant acc(tks[*].joinable);
-      invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
-      invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
-      invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
-    {
-      var tk: token<C.m>;
-      tk := tks[i-1];
-      join tk;
-      i := i-1;
-      tks := tks[0..i];
-    }
-  }
-  
-  method m()
-    requires rd(this.f,1);
-    ensures rd(this.f,1);
-  { /* do some computation */ }
-
-}