// @(#)$Id: AbstractList.refines-spec,v 1.14 2006/12/11 23:09:41 chalin Exp $

// Copyright (C) 2005 Iowa State University
//
// This file is part of the runtime library of the Java Modeling Language.
//
// This library is free software; you can redistribute it and/or
// modify it under the terms of the GNU Lesser General Public License
// as published by the Free Software Foundation; either version 2.1,
// of the License, or (at your option) any later version.
//
// This library is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
// Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with JML; see the file LesserGPL.txt.  If not, write to the Free
// Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
// 02110-1301  USA.


package java.util;

/** JML's specification of java.util.AbstractList.
 * @version $Revision: 1.14 $
 * @author Gary T. Leavens
 */
public abstract class AbstractList extends AbstractCollection implements List {

    //@ pure
    protected AbstractList();

    /*@ also
      @   protected model_program {
      @      add(size(), o); 
      @   }
      @*/
    public boolean add(/*@nullable*/ Object o);

    // specification inherited from Collection
    abstract public /*@ pure @*/ Object get(int index);

    /*@ also
      @   protected exceptional_behavior
      @     requires \typeof(this) == \type(AbstractList);
      @     assignable \nothing;
      @     signals_only UnsupportedOperationException;
      @*/
    public Object set(int index, Object element);

    /*@ also
      @   protected exceptional_behavior
      @     requires \typeof(this) == \type(AbstractList);
      @     assignable \nothing;
      @     signals_only UnsupportedOperationException;
      @*/
    public void add(int index, Object element);

    /*@ also
      @   protected exceptional_behavior
      @     requires \typeof(this) == \type(AbstractList);
      @     assignable \nothing;
      @     signals_only UnsupportedOperationException;
      @*/
    public Object remove(int index);

    // Search Operations

    // specification inherited from List
    public /*@ pure @*/ int indexOf(Object o);

    // specification inherited from List
    public /*@ pure @*/ int lastIndexOf(Object o);

    // Bulk Operations

    /*@ also
      @   protected model_program {
      @      removeRange(0, size()); 
      @   }
      @*/
    public void clear();

    // specification inherited from List
    public boolean addAll(int index, Collection c);

    // Iterators

    // specification inherited from List
    public /*@ pure @*/ Iterator iterator();

    /*@ also
      @   protected model_program {
      @      return listIterator(0);
      @   }
      @*/
    public /*@ pure @*/ ListIterator listIterator();

    // specification inherited from List
    public /*@ pure @*/ ListIterator listIterator(final int index);

    // specification inherited from List
    public /*@ pure @*/ List subList(int fromIndex, int toIndex);

    // Comparison and hashing

    // specification inherited from Object
    public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object o);

    // specification inherited from Object
    public /*@ pure @*/ int hashCode();

    /*+@ protected normal_behavior
      @  requires 0 <= fromIndex && fromIndex <= toIndex
      @              && toIndex <= size();
      @  {|
      @     requires fromIndex == toIndex;
      @     assignable \nothing;
      @   also
      @     requires fromIndex < toIndex && toIndex < size();
      @     assignable theCollection;
      @     ensures theList.equals(\old(theList.subsequence(0,fromIndex)
      @                         .concat(theList.subsequence(toIndex,size()))));
      @  |}
      @*/
    protected void removeRange(int fromIndex, int toIndex);

    protected transient int modCount;
    //+@                       in theList;
    //-@                       in _theList;

    //@ protected initially modCount == 0;
}

class SubList extends AbstractList {

    SubList(AbstractList list, int fromIndex, int toIndex);

    public Object set(int index, Object element);

    public Object get(int index);

    public int size();

    public void add(int index, Object element);

    public Object remove(int index);

    protected void removeRange(int fromIndex, int toIndex);

    public boolean addAll(Collection c);

    public boolean addAll(int index, Collection c);

    public Iterator iterator();

    public ListIterator listIterator(int index);

    public List subList(int fromIndex, int toIndex);
}



class RandomAccessSubList extends SubList implements RandomAccess {

    RandomAccessSubList(AbstractList list, int fromIndex, int toIndex);

    public List subList(int fromIndex, int toIndex);
}