001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    
006    import java.util.Enumeration;
007    import java.util.NoSuchElementException;
008    
009    
010    /**
011     * This layer describes how to implement an {@link Enumeration} in
012     * terms of a single function that returns the next element in a
013     * series, or null if the series is exhausted.<p>
014     *
015     * Using one function instead of the two used by {@link Enumeration}
016     * has the advantage of avoiding possible duplication of code to
017     * determine whether or not any elements remain in the series.<p>
018     *
019     * Limitation: <code>null</code> cannot belong to the resulting
020     * {@link Enumeration}s.<p>
021     */
022    
023    abstract class LookAheadEnum implements Enumeration {
024    
025        //@ invariant !returnsNull;
026    
027        // Object invariant: If lookAheadValid is true, then
028        // calcNextElement has already been called and its result slashed
029        // in lookAhead.
030        
031        // In particular, if lookAheadValid is true and lookAhead == null,
032        // then we are exhausted.  If lookAheadValid is true and lookAhead
033        // is non-null, then lookAhead contains the next element of the
034        // series.
035    
036    
037        //@ invariant lookAheadValid ==> moreElements == (lookAhead != null);
038        //@ spec_public
039        private boolean lookAheadValid = false;
040    
041        //@ invariant \typeof(lookAhead) <: elementType || lookAhead == null;
042        //@ spec_public
043        private Object lookAhead = null;
044    
045        /**
046         * Ensure that lookAheadValid is set, calling calcNextElement if
047         * needed.
048         */
049        //@ modifies lookAheadValid, lookAhead;
050        //@ ensures lookAheadValid;
051        private void ensureLookedAhead() {
052            if (!lookAheadValid) {
053                lookAhead = calcNextElement();
054                /*
055                 * We assume that moreElements magically predicted
056                 * calcNextElement()'s output:
057                 */
058                //@ assume moreElements == (lookAhead != null);
059                lookAheadValid = true;
060            }
061        }
062            
063    
064        /***************************************************
065         *                                                 *
066         * Creation:                                       *
067         *                                                 *
068         **************************************************/
069    
070        /**
071         * Create an look-ahead enumerator that will return the non-null
072         * results of calcNextElement().
073         */
074        //@ ensures !lookAheadValid;
075        //@ ensures lookAhead == null;              // So subclass can set elementType...
076        public LookAheadEnum() {
077            //@ set elementType = \type(Object);    // override in subclasses...
078            //@ set returnsNull = false;
079        }
080    
081        /**
082         * Create a look-ahead enumerator that will return first followed
083         * by the non-null results of calcNextElement().
084         */
085        //@ requires first != null;
086        //@ ensures moreElements;
087        //   So subclass can set elementType...:
088        //@ ensures \typeof(lookAhead) <: \typeof(first);
089        public LookAheadEnum(Object first) {
090            //@ set elementType = \type(Object);    // override in subclasses...
091            //@ set returnsNull = false;
092    
093            lookAheadValid = true;
094            lookAhead = first;
095    
096        }
097    
098    
099        /***************************************************
100         *                                                 *
101         * Handling the Enumeration interface:             *
102         *                                                 *
103         **************************************************/
104    
105        /**
106         * @return true iff any more elements exist in this enumeration.
107         */
108        //@ also
109        //@ private behavior
110        //@   modifies lookAheadValid, lookAhead;
111        //@   ensures \result == (lookAhead != null);
112        public final boolean hasMoreElements() {
113            ensureLookedAhead();
114    
115            return lookAhead != null;
116        }
117    
118        //@ also
119        //@ public behavior
120        //@   modifies \everything;
121            //@   signals_only NoSuchElementException;
122        //@   signals (NoSuchElementException) (lookAhead == null);
123        //    Should be:
124        //    modifies lookAheadValid, lookAhead;
125        //    but because NoSuchElementException has no spec, then the
126        //    constructor has the default modifies clause of \everything.
127        public final Object nextElement() {
128            ensureLookedAhead();
129    
130            if (lookAhead == null)
131                throw new NoSuchElementException();
132    
133            lookAheadValid = false;
134            return lookAhead;
135        } //@ nowarn Exception;
136    
137    
138        /***************************************************
139         *                                                 *
140         * Calculating the next element:                   *
141         *                                                 *
142         **************************************************/
143    
144        /**
145         * Compute the next element in the series, or return null if the
146         * series is exhausted.
147         *
148         * This function will never be called again once it returns null.
149         */
150        //---@ modifies \nothing;
151        //@ ensures \typeof(\result) <: elementType || \result==null;
152        protected abstract Object calcNextElement();
153    
154    }