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 }