001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.filespace; 004 005 006 import java.util.Enumeration; 007 import java.util.NoSuchElementException; 008 009 010 /** 011 * This layer describes how to implement an {@link Enumeration} in 012 * terms of a single function that returns the next element in a 013 * series, or null if the series is exhausted.<p> 014 * 015 * Using one function instead of the two used by {@link Enumeration} 016 * has the advantage of avoiding possible duplication of code to 017 * determine whether or not any elements remain in the series.<p> 018 * 019 * Limitation: <code>null</code> cannot belong to the resulting 020 * {@link Enumeration}s.<p> 021 */ 022 023 abstract class LookAheadEnum implements Enumeration { 024 025 //@ invariant !returnsNull; 026 027 // Object invariant: If lookAheadValid is true, then 028 // calcNextElement has already been called and its result slashed 029 // in lookAhead. 030 031 // In particular, if lookAheadValid is true and lookAhead == null, 032 // then we are exhausted. If lookAheadValid is true and lookAhead 033 // is non-null, then lookAhead contains the next element of the 034 // series. 035 036 037 //@ invariant lookAheadValid ==> moreElements == (lookAhead != null); 038 //@ spec_public 039 private boolean lookAheadValid = false; 040 041 //@ invariant \typeof(lookAhead) <: elementType || lookAhead == null; 042 //@ spec_public 043 private Object lookAhead = null; 044 045 /** 046 * Ensure that lookAheadValid is set, calling calcNextElement if 047 * needed. 048 */ 049 //@ modifies lookAheadValid, lookAhead; 050 //@ ensures lookAheadValid; 051 private void ensureLookedAhead() { 052 if (!lookAheadValid) { 053 lookAhead = calcNextElement(); 054 /* 055 * We assume that moreElements magically predicted 056 * calcNextElement()'s output: 057 */ 058 //@ assume moreElements == (lookAhead != null); 059 lookAheadValid = true; 060 } 061 } 062 063 064 /*************************************************** 065 * * 066 * Creation: * 067 * * 068 **************************************************/ 069 070 /** 071 * Create an look-ahead enumerator that will return the non-null 072 * results of calcNextElement(). 073 */ 074 //@ ensures !lookAheadValid; 075 //@ ensures lookAhead == null; // So subclass can set elementType... 076 public LookAheadEnum() { 077 //@ set elementType = \type(Object); // override in subclasses... 078 //@ set returnsNull = false; 079 } 080 081 /** 082 * Create a look-ahead enumerator that will return first followed 083 * by the non-null results of calcNextElement(). 084 */ 085 //@ requires first != null; 086 //@ ensures moreElements; 087 // So subclass can set elementType...: 088 //@ ensures \typeof(lookAhead) <: \typeof(first); 089 public LookAheadEnum(Object first) { 090 //@ set elementType = \type(Object); // override in subclasses... 091 //@ set returnsNull = false; 092 093 lookAheadValid = true; 094 lookAhead = first; 095 096 } 097 098 099 /*************************************************** 100 * * 101 * Handling the Enumeration interface: * 102 * * 103 **************************************************/ 104 105 /** 106 * @return true iff any more elements exist in this enumeration. 107 */ 108 //@ also 109 //@ private behavior 110 //@ modifies lookAheadValid, lookAhead; 111 //@ ensures \result == (lookAhead != null); 112 public final boolean hasMoreElements() { 113 ensureLookedAhead(); 114 115 return lookAhead != null; 116 } 117 118 //@ also 119 //@ public behavior 120 //@ modifies \everything; 121 //@ signals_only NoSuchElementException; 122 //@ signals (NoSuchElementException) (lookAhead == null); 123 // Should be: 124 // modifies lookAheadValid, lookAhead; 125 // but because NoSuchElementException has no spec, then the 126 // constructor has the default modifies clause of \everything. 127 public final Object nextElement() { 128 ensureLookedAhead(); 129 130 if (lookAhead == null) 131 throw new NoSuchElementException(); 132 133 lookAheadValid = false; 134 return lookAhead; 135 } //@ nowarn Exception; 136 137 138 /*************************************************** 139 * * 140 * Calculating the next element: * 141 * * 142 **************************************************/ 143 144 /** 145 * Compute the next element in the series, or return null if the 146 * series is exhausted. 147 * 148 * This function will never be called again once it returns null. 149 */ 150 //---@ modifies \nothing; 151 //@ ensures \typeof(\result) <: elementType || \result==null; 152 protected abstract Object calcNextElement(); 153 154 }