1 files changed, 0 insertions, 150 deletions
diff --git a/Chalice/tests/examples/iterator.chalice b/Chalice/tests/examples/iterator.chalice
deleted file mode 100644
index fd5d0352..00000000
--- a/Chalice/tests/examples/iterator.chalice
+++ /dev/null
@@ -1,150 +0,0 @@
-class List module Collections {
-  var contents: seq<int>;
-
-  method init()
-    requires acc(contents);
-    ensures valid && size(100)==0;
-  {
-    contents := nil<int>;
-    fold valid; 
-  }
-
-  method add(x: int) 
-    requires valid;
-    ensures valid && size(100) == old(size(100)+1) && get(size(100)-1, 100) == x;
-    ensures forall i in [0..size(100)-1] :: get(i, 100) == old(get(i, 100));
-  {
-    unfold valid;
-    contents := contents ++ [x];
-    fold valid;
-  }
-
-  function get(index: int, f: int): int 
-    requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));
-    ensures forall i in [1..f] :: get(index, f) == get(index, i);
-  {
-    unfolding acc(valid, f) in contents[index]
-  }
-
-  function size(f: int): int 
-    requires 0<f && f<=100 && acc(valid, f);
-    ensures 0<=result;
-    ensures forall i in [1..f] :: size(f) == size(i);
-  {
-    unfolding acc(valid, f) in |contents|
-  }
-
-  predicate valid {
-    acc(contents)
-  }
-}
-
-class Iterator module Collections {
-  var list: List;
-  var index: int;
-  var frac: int;
-
-  method init(l: List, f: int)
-    requires 0<f && f<=100;
-    requires acc(list) && acc(index) && acc(frac);
-    requires l!=null;
-    requires acc(l.valid, f);
-    ensures valid;
-    ensures getList()==l;
-    ensures getFraction()==f;
-  {
-    list := l;
-    this.index := 0;
-    frac := f;
-    fold valid;
-  }
-
-  method next() returns (rt: int) 
-    requires valid && hasNext();
-    ensures valid;
-    ensures getList()==old(getList());
-    ensures getFraction()==old(getFraction());
-  {
-    unfold valid;
-    rt := list.get(index, frac);
-    index := index + 1;
-    fold valid;
-  }
-
-  method dispose()
-    requires valid;
-    ensures acc(old(getList()).valid, old(getFraction()));
-  {
-    unfold valid;
-  }
-
-  function hasNext(): bool 
-    requires valid;
-  {
-    unfolding valid in index<list.size(frac)
-  }
-
-  function getFraction(): int
-    requires valid;
-    ensures 0<result && result<=100;
-  {
-    unfolding valid in frac
-  }
-
-  function getList(): List
-    requires valid;
-    ensures getList()!=null;
-  {
-    unfolding valid in list
-  }
-
-  predicate valid
-  {
-    acc(list) && acc(index) && acc(frac) && 0<frac && frac<=100 && list!=null && acc(list.valid, frac) && 0<=index && index<=list.size(frac)
-  }
-}
-
-class Program module Main {
-  method main(){
-    var tmp: int;
-    //create a new list
-    var list := new List;
-    call list.init();
-    call list.add(5);
-    call list.add(6);
- 
-    // create a new iterator
-    var iter1 := new Iterator;
-    assert list!=null; // needed here: triggering problem?
-    assert list.size(100)==2;
-    assert list.size(50)==2;
-    call iter1.init(list, 10);
-
-    // create a second iterator
-    var iter2 := new Iterator;
-    assert list!=null; // needed here: triggering problem?
-    call iter2.init(list, 10);
-    
-    // iterate over the list
-    while(iter1.hasNext())
-      invariant iter1.valid && iter1.getList()==list && iter1.getFraction()==10;
-    {
-      call tmp := iter1.next();
-    }
-
-    // iterate over the list
-    while(iter2.hasNext())
-      invariant iter2.valid && iter2.getList()==list && iter2.getFraction()==10;
-    {
-      call tmp := iter2.next();
-    }
-
-    // dispose the iterators
-    call iter1.dispose();
-    call iter2.dispose();
-
-    // full access to the list
-    assert list.valid;
-    assert list.size(50)==2;
-  }
-}