// @(#)$Id: LinkedList.refines-spec,v 1.16 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;

//@ model import org.jmlspecs.models.*;

/** JML's specification of java.util.LinkedList.
 * @author Katie Becker
 * @author Gary T. Leavens
 */

public class LinkedList extends AbstractSequentialList
    implements List, Cloneable, java.io.Serializable
{
	
    /*+@ public normal_behavior
      @   assignable theCollection;
      @   ensures theList != null && theList.isEmpty();
      @*/
    /*-@ public normal_behavior
      @   assignable _theCollection;
      @   ensures _theList != null && isEmpty();
      @*/
    public LinkedList();
          
    /*+@   public normal_behavior
      @     requires c != null;
      @     assignable theCollection;
      @     ensures theList != null; 
      @     ensures JMLEqualsSequence.convertFrom(c).equals(theList);
      @ also
      @   public exceptional_behavior
      @     requires c == null;
      @     assignable theCollection;
      @     signals_only NullPointerException;
      @*/
    /*-@   public normal_behavior
      @     requires c != null;
      @     assignable _theCollection;
      @     ensures _theList != null; 
      @     ensures _theCollection == _theList;
      @ also
      @   public exceptional_behavior
      @     requires c == null;
      @     assignable _theCollection;
      @     signals_only NullPointerException;
      @*/
    public LinkedList(Collection c);
    
    /*+@  public normal_behavior
      @    requires !theList.isEmpty();
      @    ensures (\result == null) || \typeof(\result) <: elementType;
      @    ensures \result.equals(theList.itemAt(0));
      @ also
      @  public exceptional_behavior
      @    requires theList.isEmpty();
      @    signals_only NoSuchElementException;
      @*/
    /*-@  public normal_behavior
      @    requires !isEmpty();
      @    ensures (\result == null) || \typeof(\result) <: elementType;
      @    ensures \result.equals(_theList[0]);
      @ also
      @  public exceptional_behavior
      @    requires isEmpty();
      @    signals_only NoSuchElementException;
      @*/
    public /*@ pure @*/ Object getFirst();
    
    /*+@  public normal_behavior
      @    requires !theList.isEmpty();
      @    ensures (\result == null) || \typeof(\result) <: elementType;
      @    ensures \result.equals(theList.itemAt((int)(theList.int_size()-1)));
      @ also
      @  public exceptional_behavior
      @    requires theList.isEmpty();
      @    signals_only NoSuchElementException; 
      @*/
    public /*@ pure @*/ Object getLast();

    /*+@  public normal_behavior
      @    requires !theList.isEmpty();
      @    assignable theCollection;
      @    ensures \result.equals(\old(theList.itemAt(0)));
      @    ensures theList.equals(\old(theList).removeItemAt(0));
      @    ensures ((\result == null) || \typeof(\result) <: elementType);
      @ also
      @  public exceptional_behavior
      @    requires theList.isEmpty();
      @    assignable \nothing;
      @    signals_only NoSuchElementException;
      @*/    
    public Object removeFirst();
 
    /*+@  public behavior
      @    requires !theList.isEmpty();
      @    assignable theCollection;
      @    ensures \result.equals(\old(theList.itemAt((int)(theList.int_size()-1))));
      @    ensures theList
      @           .equals(\old(theList.removeItemAt((int)(theList.int_size()-1))));
      @    ensures ((\result == null) || \typeof(\result) <: elementType);
      @ also 
      @  public exceptional_behavior
      @    requires theList.isEmpty();
      @    assignable \nothing;
      @    signals_only NoSuchElementException;
      @*/     
    public Object removeLast();
  
    /*+@ public normal_behavior
      @   assignable theCollection;
      @   ensures theList.equals(\old(theList.insertFront(o)));
      @   ensures_redundantly theList.itemAt(0).equals(o);
      @*/    
    public void addFirst(Object o);

    /*+@ public normal_behavior
      @   assignable theCollection;
      @   ensures theList.equals(\old(theList.insertBack(o)));
      @   ensures_redundantly theList.itemAt((int)(theList.int_size()-1)).equals(o);
      @*/     
    public void addLast(Object o);
    
    // -- all other methods are specified by List --
    //@ pure
    public boolean contains(/*@nullable*/ Object o);
    
    //@ pure
    public int size();
    
    public boolean add(/*@nullable*/ Object o);

    public boolean remove(/*@nullable*/ Object o);
    
    public boolean addAll(Collection c);
    
    public boolean addAll(int index, Collection c);
    
    public void clear();
    
    //@ pure
    public Object get(int index);
    
    public Object set(int index, Object element);
    
    public void add(int index, Object element);
    
    public Object remove(int index);
    
    //@ pure
    public int indexOf(Object o);
    
    //@ pure
    public int lastIndexOf(Object o);
    
    //@ pure
    public ListIterator listIterator(int index);
    
    /*+@ also
      @   public normal_behavior
      @       ensures \result instanceof LinkedList && \fresh(\result)
      @          && ((LinkedList)\result).equals(this);
      @       ensures_redundantly \result != this;
      @*/
    public /*@ pure @*/ Object clone();

    //@ pure
    public Object[] toArray();
    
    public Object[] toArray(Object[] a);
}