001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.filespace;
004    
005    import java.util.*;
006    
007    /**
008     * This class simply implements an enumeration with no elements.
009     */
010    
011    class EmptyEnum implements Enumeration
012    {
013        //@ represents moreElements <- false;
014    
015        //@ invariant !moreElements;
016        //@ invariant !returnsNull;
017    
018        EmptyEnum() {
019            //@ set returnsNull = false;
020            //@ set elementType = \type(Object);
021        }
022    
023        /**
024         * @return true iff any more elements exist in this enumeration.
025         */
026        //@ also
027        //@ public normal_behavior
028        //@   ensures_redundantly \result == false;
029        //@ pure
030        public boolean hasMoreElements() {
031            return false;
032        }
033    
034        /**
035         * Always throws a NoSuchElementException since there are no
036         * elements.
037         */
038        //@ also
039        //@ public exceptional_behavior
040        //@   signals_only NoSuchElementException;
041        //@   signals (NoSuchElementException) true;
042        //@ pure
043        public Object nextElement() {
044          throw new NoSuchElementException();
045        } //@ nowarn Exception;
046    }