package java.util;

/*@
predicate list(List l, list<Object> v);

predicate iter(Iterator i, List l, list<Object> v, int index);

lemma void iter_dispose(Iterator iter);
 requires iter(iter, ?l, ?v, ?i);
 ensures list(l, v);
@*/
interface List{
  boolean add(Object element);
  //@ requires list(this, ?v);
  //@ ensures list(this, append(v, cons(element, nil))) &*& result;
  boolean remove(Object element);
  //@ requires list(this, ?v);
  //@ ensures mem(element, v) ?list(this, remove(element, v)):list(this,v);
  Iterator iterator();
  //@ requires list(this, ?v);
  //@ ensures result != null &*& iter(result, this, v, 0);
}
interface Iterator{
  boolean hasNext();
  //@ requires iter(this, ?l, ?v, ?i);
  //@ ensures iter(this, l, v, i) &*& result == (i < length(v));
  Object next();
  //@ requires iter(this, ?l, ?v, ?i) &*& i < length(v);
  //@ ensures iter(this, l, v, i + 1) &*& result==nth(i, v);
  
}
public class ArrayList implements List{
  ArrayList();
  //@ requires emp;
  //@ ensures list(this, nil);
}