// @(#) $Id: TwoWayIterator.jml,v 1.9 2005/12/06 19:55:00 chalin Exp $

// Copyright (C) 1998, 1999 Iowa State University

// This file is part of JML

// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.

// JML 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 General Public License for more details.

// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING.  If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.

// Author:  Clyde Ruby

package org.jmlspecs.samples.list.list3;

//@ refine "TwoWayIterator.jml-refined";

//@ model import org.jmlspecs.models.JMLObjectBag;
//@ model import org.jmlspecs.models.JMLObjectSequence;

import org.jmlspecs.samples.list.node.OneWayNode;
import org.jmlspecs.samples.list.node.TwoWayNode;
import org.jmlspecs.samples.list.iterator.RestartableIterator;

// FIXME: adapt this file to non-null-by-default and remove the following modifier.
/*@ nullable_by_default @*/ 
public class TwoWayIterator implements RestartableIterator {
    protected TwoWayNode firstLink_;
  /*@                    in currElem, uniteratedElems, iteratedElems;
    @                    maps firstLink_.entries \into unchanged;
    @*/

  //@ protected invariant firstLink_ != null;

    protected TwoWayNode currLink_;
  /*@              in currIndex, currElem, uniteratedElems, iteratedElems;
    @              maps currLink_.entries \into unchanged, uniteratedElems;
    @              maps currLink_.prevEntries \into unchanged, iteratedElems;
    @*/

    protected TwoWayNode lastLink_;
  //@                    in uniteratedElems;

   // using allButFirst is necessary because the first link is a sentinel.

  //@ protected represents theList <- firstLink_.allButFirst;

  /*@ protected represents uniteratedElems <-
    @            (currIndex <= 0)?
    @            JMLObjectBag.convertFrom( theList )
    @          : JMLObjectBag.convertFrom( theList.removePrefix(currIndex) );
    @*/

  /*@ protected represents iteratedElems <-
    @            (currIndex <= 0)?
    @            JMLObjectBag.EMPTY
    @          : JMLObjectBag.convertFrom( theList.prefix(currIndex) );
    @*/

  /* @ protected represents unchanged <- 
    @        (currIndex <= 0)?
    @        theList.equals( currLink_.getNextNode().entries ) 
    @      : theList.equals(
    @            currLink_.prevEntries.trailer().concat(currLink_.entries) );
    @ */

  /*@ protected represents currElem <- 
    @        ( 0 <= currIndex && currIndex < theList.int_length())?
    @        theList.itemAt(currIndex) 
    @      : null;
    @ */
  //@ protected represents currIndex <- indexOf(currLink_);

  /*@ 
      protected pure model int indexOf(OneWayNode link) {
          OneWayNode currLink = firstLink_;
     
          int index = -1;
          //@  maintaining currLink != link;
          //@  decreasing theList.int_length() - indexOf(currLink);
          while (currLink != null && currLink != link) {
              index++;
              currLink = currLink.getNextNode();
          }
          // System.out.println("indexOf("+link+")="+index);
          return index;
      }
    @*/

  /*@ protected code normal_behavior
    @   assignable currElem, uniteratedElems, iteratedElems, currIndex;
    @   ensures theList.isEmpty() && currIndex == 0;
    @*/
    protected TwoWayIterator();

}