/* Copyright (C) 1998 H. Conrad Cunningham. All rights reserved. */ package SoftwareInterfaces; /** * A class that provides an enumeration iterator for the array-based * ranked sequence abstract data type * * @author H. Conrad Cunningham * @version 1 June 1998 */ public class ArrayRankedSeqEnum implements java.util.Enumeration { /** * Constructs an enumeration iterator for instances of class * ArrayRankedSeq. * * @param seq the array of objects representing the sequence * @param len the number of elements at the front of seq * containing the sequence elements *

Preconditon:0 <= len <= seq.length.
* seq is the internal array of an * ArrayRankedSeq instance with length() *

len>.
     *

Postcondition: 
     *

enumerator is initialized to the first element (if any) of the 
     *     sequence
     */
    public ArrayRankedSeqEnum (Object[] seq, int len)
    {   theSeq = seq;  seqLength = len; next = 0; }


    /**
     * Determines whether more elements from the sequence remain to be 
     * enumerated by this enumerator.
     *
     * @return true if more elements exist; false otherwise
     */
    public boolean hasMoreElements()
    {   return (next != seqLength); }


    /**
     * Retrieves the next unprocessed element of this enumeration of 
     * the sequence. 
     *
     *

Preconditon: 
     *

hasMoreElements()
     *
     *

Postcondition: 
     *

enumerator is advanced so that the succeeding element (if any)
     *     will be returned on any future call.
     */
    public Object nextElement()
    {   try // AssertionViolation not in Enumeration interface definition
        {   Assert.inv(0 <= next && next <= seqLength 
		       && seqLength <= theSeq.length); 
        }
        catch(AssertionViolation m)
	{   System.out.println("Invariant Violation exception " +
			       "in ArrayRankedSeqEnum.nextElement.\n" +
			       "        Internal Error");
	    System.exit(1);
	}
        try // AssertionViolation not in Enumeration interface definition
        {   Assert.pre(hasMoreElements()); }
        catch(AssertionViolation m)
	{   System.out.println("Precondition Violation exception " +
			       "in ArrayRankedSeqEnum.nextElement.");
	    System.exit(1);
	}
        Object ret = theSeq[next];
        next++;
	return ret;
    }
    
    /* Invariant:  0 <= next <= seqLength <= theSeq.length 
                   && theSeq not changed since creation of this enumerator
                   && (for 0 <= r < seqLength, 
                          theSeq[r] == element at rank r of the sequence)
    */

    private int seqLength;   // number of elements in the sequence
    private Object[] theSeq; // array to store the sequence elements
    private int next;        // next unprocessed element of the enumeration
}