1 files changed, 0 insertions, 202 deletions
diff --git a/Chalice/tests/examples/producer-consumer.chalice b/Chalice/tests/examples/producer-consumer.chalice
deleted file mode 100644
index 25253bfb..00000000
--- a/Chalice/tests/examples/producer-consumer.chalice
+++ /dev/null
@@ -1,202 +0,0 @@
-class Program {
-  method main(){
-    var buffer := new Queue;
-    call buffer.init();
-    share buffer;
-
-    var producer := new Producer;
-    call producer.init(buffer);
-    fork tkP := producer.run();
-
-    var consumer := new Consumer;
-    call consumer.init(buffer);
-    fork tkC := consumer.run();
-
-    join tkP;
-    join tkC;
-  
-    acquire buffer;
-    unshare buffer;
-
-    var tmp := buffer.size();
-  }
-}
-
-class Producer module Producer {
-  var buffer: Queue;
-
-  method init(buff: Queue)
-    requires acc(buffer) && buff!=null;
-    ensures valid && getBuffer()==buff;
-  {
-    buffer := buff;
-    fold valid;
-  }
-
-  method run()
-    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
-    ensures rd(old(getBuffer()).mu);
-  {
-    var tmp: int;
-
-    while(true)
-      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
-    {
-      unfold valid;
-      acquire buffer;
-      call buffer.enqueue(5);
-      release buffer;
-      fold valid;
-    }
-    unfold valid;
-  }
-
-  function getBuffer(): Queue
-    requires valid;
-    ensures result!=null;
-  {
-    unfolding valid in buffer
-  }
-
-  predicate valid {
-    acc(buffer) && buffer!=null
-  }
-}
-
-class Consumer module Consumer {
-  var buffer: Queue;
-
-  method init(buff: Queue)
-    requires acc(buffer) && buff!=null;
-    ensures valid && getBuffer()==buff;
-  {
-    buffer := buff;
-    fold valid;
-  }
-
-  method run()
-    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
-    ensures rd(old(getBuffer()).mu);
-  {
-    while(true)
-      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
-    {
-      unfold valid;
-      acquire buffer;
-      if(0<=buffer.size()){
-        call buffer.enqueue(5);
-      }
-      release buffer;
-      fold valid;
-    }
-    unfold valid;
-  }
-
-  function getBuffer(): Queue
-    requires valid;
-    ensures result!=null;
-  {
-    unfolding valid in buffer
-  }
-
-  predicate valid {
-    acc(buffer) && buffer!=null
-  }
-}
-
-class Queue module Queue {
-  var contents: List;
-
-  invariant valid;
-
-  method init()
-    requires acc(contents);
-    ensures valid;
-    ensures size()==0;
-  {
-    contents := new List;
-    call contents.init();
-    fold valid;
-  }
-
-  method enqueue(x: int) 
-    requires valid;
-    ensures valid;
-    ensures size() == old(size())+1;
-  {
-    unfold valid;
-    call contents.add(x);
-    fold valid;
-  }
-
-  method dequeue() returns (rt: int)
-    requires valid && 0<size();
-    ensures valid;
-    ensures size() == old(size())-1;
-  {
-    unfold valid;
-    call rt := contents.removeFirst();
-    fold valid;
-  }
-
-  function size(): int
-    requires valid;
-  {
-    unfolding valid in contents.size()
-  }
-
-  predicate valid {
-    acc(contents) && contents!=null && contents.valid
-  }
-}
-
-class List module Collections {
-  var contents: seq<int>;
-
-  method init()
-    requires acc(contents);
-    ensures valid && size()==0;
-  {
-    contents := nil<int>;
-    fold valid; 
-  }
-
-  method add(x: int) 
-    requires valid;
-    ensures valid && size() == old(size()+1) && get(size()-1) == x;
-    ensures forall i in [0..size()-1] :: get(i) == old(get(i));
-  {
-    unfold valid;
-    contents := contents ++ [x];
-    fold valid;
-  }
-
-  method removeFirst() returns (rt: int) 
-    requires valid && 0<size();
-    ensures valid && size() == old(size()-1);
-    ensures forall i in [0..size()] :: get(i) == old(get(i+1));
-  {
-    unfold valid;
-    rt := contents[0];
-    contents := contents[1..];
-    fold valid;
-  }
-
-
-  function get(index: int): int 
-    requires rd(valid) && 0<=index && index<size();
-  {
-    unfolding rd(valid) in contents[index]
-  }
-
-  function size(): int 
-    requires rd(valid);
-    ensures 0<=result;
-  {
-    unfolding rd(valid) in |contents|
-  }
-
-  predicate valid {
-    acc(contents)
-  }
-}