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 }