import java.util.Iterator;
import java.util.NoSuchElementException;

/**
 *  Iterateur en lecture seule pour les tableaux (l'opération <code>remove</code>
 *  leve une exception <code>UnsupportedOperationException</code>).
 *
 * @author     Marc Champesme
 * @version    12 janvier 2005
 * @since      12 janvier 2005
 */
public class TableauIterator implements Iterator {
	/*@
	  @ private represents moreElements <- (index < nbElements);
	  @*/
	private Object[] tab;
	private int index;
	private int nbElements;


	/**
	 *  Initialise un itérateur sur les <code>nbElements</code> premiers éléments
	 *  du tableau spécifié.
	 *
	 * @param  tab         le tableau dont cet itérateur doit retourner les
	 *      éléments
	 * @param  nbElements  le nombre d'éléments sur lequel ce tableau doit itérer
	 */
	/*@
	  @ requires tab != null;
	  @ requires tab.length >= nbElements;
	  @ requires nbElements >= 0;
	  @ ensures (nbElements > 0) <==> moreElements;
	  @
	  @*/
	public TableauIterator(Object[] tab, int nbElements) {
		this.tab = tab;
		this.nbElements = nbElements;
	}


	/**
	 *  Renvoie <code>true</code> s'il reste des éléments pour cette itération.
	 *  (Autrement dit, renvoie <code>true</code> si <code>next</code> renverrait
	 *  un élément plutot que de lever une exception).
	 *
	 * @return    <code>true</code> s'il reste des éléments
	 */
	public boolean hasNext() {
		return index < nbElements;
	}


	/**
	 *  Renvoie l'élément suivant pour cette itération.
	 *
	 * @return                          l'élément suivant pour cette itération
	 * @throws  NoSuchElementException  s'il ne reste plus d'élément pour cette
	 *      itération.
	 */
	public Object next() {
		if (!hasNext()) {
			throw new NoSuchElementException("Plus d'éléments");
		}
		return tab[index++];
	}


	/**
	 *  Lève toujours une <code>UnsupportedOperationException</code>.
	 */
	public void remove() {
		throw new UnsupportedOperationException("Iterateur en lecture seule");
	}
}