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 }