package mylist; 

public interface List { 

  /**
   * Returns the number of elements in the list.
   *
   * @pre  true
   * @post @nochange 
   */
  public int size();

  /**
   * Returns true if and only if the list is empty.
   *
   * @pre  true
   * @post @result <=> size() > 0 
   * @post @nochange 
   */
  public boolean isEmpty();

  /**
   * Returns the i-th element in the list.
   *
   * @pre i >= 0 && i < size()
   * @post @nochange 
   */ 
  public Object element(int i);

  /**
   * Returns the first element in the list.
   *
   * @pre  !isEmpty()
   * @post @result == element(0)
   * @post @nochange 
   */ 
  public Object head();

  /**
   * Returns the last element in the list.
   *
   * @pre  !isEmpty()
   * @post @result == element(size() - 1)
   * @post @nochange 
   */ 
  public Object last();

  /**
   * Inserts a new element into the list at the i-th position.
   *
   * @pre  item != null && i >= 0 && i <= size()
   * @post size() == size()@pre + 1
   * @post @forall k : [0 .. size() - 1] @ 
   *         (k < i ==> element(k)@pre == element(k)) &&    
   *         (k == i ==> item@pre == element(k)) &&    
   *         (k > i ==> element(k - 1)@pre == element(k)
   */ 
  public void insert(Object item, int i);

  /**
   * Inserts a new element at the head of the list.
   *
   * @pre  item != null
   * @post size() == size()@pre + 1
   * @post item@pre == element(0)
   * @post @forall k : [1 .. size() - 1] @ element(k - 1)@pre == element(k)
   */ 
  public void insertHead(Object item);

  /**
   * Inserts a new element at the end of the list.
   *
   * @pre  item != null
   * @post size() == size()@pre + 1
   * @post item@pre == element(size() - 1)
   * @post @forall k : [0 .. size() - 2] @ element(k)@pre == element(k)
   */ 
  public void insertLast(Object item);

  /**
   * Remove the element at the i-th position. 
   *
   * @pre  size() > 0
   * @pre  i >= 0 && i < size()
   * @post @result = element(i)@pre
   * @post size() == size()@pre - 1
   * @post @forall k : [0 .. size() - 1] @
   *         (k < i ==> element(k)@pre == element(k)) &&
   *         (k >= i ==> element(k + 1)@pre == element(k))
   */
  public Object remove(int i);

  /**
   * Remove the element at the head. 
   *
   * @pre  size() > 0
   * @post @result = element(0)@pre
   * @post @forall k : [1 .. size() - 1] @ element(k + 1)@pre == element(k)
   */
  public Object removeHead();

  /**
   * Remove the element at the end. 
   *
   * @pre  size() > 0
   * @post @result = element(size() - 1)@pre
   * @post @forall k : [0 .. size() - 1] @ element(k)@pre == element(k)
   */
  public Object removeLast();

}