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;
  }
}