001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    
006    import java.util.Enumeration;
007    
008    /**
009     * A FilterEnum filters an underlying Enumeration using a client
010     * supplied Filter.
011     */
012    
013    
014    class FilterEnum extends LookAheadEnum {
015    
016        /** The underlying Enumeration: */
017        //@ invariant underlyingEnum != null;
018        //@ invariant !underlyingEnum.returnsNull;
019        //@ invariant underlyingEnum.owner == this;
020        protected Enumeration underlyingEnum;
021    
022        // We inherit our properties from the underlying Enumeration:
023        //@ invariant elementType == underlyingEnum.elementType;
024    
025    
026        /** The filter we are using: */
027        //@ invariant filter != null;
028        //@ invariant filter.acceptedType == elementType;
029        public Filter filter;
030    
031    
032        /***************************************************
033         *                                                 *
034         * Creation:                                       *
035         *                                                 *
036         **************************************************/
037    
038        /**
039         * Filter the Enumeration E using Filter F:
040         */
041        //@ requires E != null && F != null;
042        //@ requires !E.returnsNull;
043        //@ requires E.owner == null;
044        //@ requires E.elementType == F.acceptedType;
045        //@ ensures elementType == E.elementType;
046        public FilterEnum(Enumeration E, Filter F) {
047            super();
048    
049            //@ set E.owner = this;
050            underlyingEnum = E;
051            filter = F;
052    
053            //@ set elementType = E.elementType;
054        }
055    
056    
057        /***************************************************
058         *                                                 *
059         * Calculating the next element:                   *
060         *                                                 *
061         **************************************************/
062    
063        /**
064         * Compute the next element in the series, or return null if the
065         * series is exhausted.
066         */
067    
068        protected Object calcNextElement() {
069            while (underlyingEnum.hasMoreElements()) {
070                Object next = underlyingEnum.nextElement();
071    
072                if (filter.accept(next))
073                    return next;
074            }
075    
076            return null;
077        }
078    }