    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    }