    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    }