// @(#)$Id: _ValueType_AbstractFilteringIteratorDecorator.java-generic,v 1.11 2005/12/24 21:20:31 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 org.jmlspecs.jmlunit.strategies;

import java.util.NoSuchElementException;

/** An filtering decorator for an indefinite iterator over type _ValueType_.
 * @author Gary T. Leavens
 */
// FIXME: adapt this file to non-null-by-default and remove the following modifier.
/*@ nullable_by_default @*/ 
public abstract class _ValueTypeCap_AbstractFilteringIteratorDecorator
    extends _ValueTypeCap_AbstractIterator
{
    private /*@ spec_public non_null @*/ _ValueTypeCap_Iterator rawElems;
    //@ in objectState; maps rawElems.objectState \into objectState;

    //@ public ghost boolean dented = false;

    //@ public invariant !dented ==> (atEnd() <==> rawElems.atEnd());
    /*@ public invariant !dented ==>
      @                   (!atEnd() ==> get().equals(rawElems.get()));
      @ public invariant_redundantly !dented ==>
      @                 (!atEnd() ==>
      @                 new _LangType_(get_ValueTypeCap_())
      @                 .equals(new _LangType_(rawElems.get_ValueTypeCap_())));
      @*/

    /** Initialize this iterator decorator */
    /*@ public normal_behavior
      @   requires iter != null;
      @   assignable rawElems, objectState, owner;
      @   ensures (* rawElems is a clone of iter *);
      @   ensures owner == null;
      @*/
    public _ValueTypeCap_AbstractFilteringIteratorDecorator
        (_ValueTypeCap_Iterator iter)
    {
        rawElems = (_ValueTypeCap_Iterator) iter.clone();
        //@ set rawElems.owner = this;
        //@ set owner = null;
        setCursor();
    }

    /** Partially intialize this iterator decorator, with a call to
     * initialize needed after this call. */
    /*@ public normal_behavior
      @   requires iter != null;
      @   assignable rawElems, dented, owner;
      @   ensures (* rawElems is a clone of iter *) && dented;
      @   ensures owner == null;
      @*/
    public _ValueTypeCap_AbstractFilteringIteratorDecorator
        (_ValueTypeCap_Iterator iter, _ValueType_ ignored)
    {
        //@ set dented = true;
        rawElems = (_ValueTypeCap_Iterator) iter.clone();
        //@ set rawElems.owner = this;
        //@ set owner = null;
    }

    /** Complete initialization of this object. */
    //@ assignable objectState, dented;
    //@ ensures !dented;
    //@ ensures !atEnd() ==> approve(get_ValueTypeCap_());
    public void initialize() {
        setCursor();
        //@ set dented = false;
    }

    /** Set the cursor to the next element that is approved, if any. */
    //@ assignable objectState;
    //@ ensures !rawElems.atEnd() ==> approve(rawElems.get_ValueTypeCap_());
    private void setCursor() {
        while (!rawElems.atEnd() && !approve(rawElems.get_ValueTypeCap_())) {
            rawElems.advance();
        }
    }

    /** Return true if the element is to be returned by the
     * get_ValueTypeCap_() method. */
    //@ public normal_behavior
    //@   assignable \nothing;
    public abstract /*@ pure @*/ boolean approve(_ValueType_ elem);

    // doc comment inherited
    /*@ also public normal_behavior
      @   assignable \nothing;
      @   ensures \result == rawElems.atEnd();
      @*/
    public /*@ pure @*/ boolean atEnd() {
        return rawElems.atEnd();
    }

    /** Return the current approved element. */
    public /*@ pure @*/ _ValueType_ get_ValueTypeCap_()
        throws NoSuchElementException
    {
        return rawElems.get_ValueTypeCap_();
    }

    // doc comment inherited
    //@ also public normal_behavior
    //@   assignable objectState;
    //@   ensures !atEnd() ==> approve(get_ValueTypeCap_());
    public void advance() {
        rawElems.advance();
        setCursor();
    }

    public /*@ non_null @*/ Object clone() {
        _ValueTypeCap_AbstractFilteringIteratorDecorator ret
            = (_ValueTypeCap_AbstractFilteringIteratorDecorator) super.clone();
        ret.rawElems = (_ValueTypeCap_Iterator) rawElems.clone();
        return ret;
    }

    public /*@ non_null @*/ String toString() {
        return "_ValueTypeCap_AbstractFilteringIteratorDecorator("
            + rawElems + ")";
    }
}