/[eiffelstudio]/branches/eth/eve/Src/library/base/base2/iterator/v_iterator.e
ViewVC logotype

Contents of /branches/eth/eve/Src/library/base/base2/iterator/v_iterator.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94771 - (show annotations)
Thu Apr 3 12:37:44 2014 UTC (5 years, 6 months ago) by polikarn
File size: 6578 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
1 note
2 description: "[
3 Iterators to read from a container in linear order.
4 Indexing starts from 1.
5 ]"
6 author: "Nadia Polikarpova"
7 model: target, sequence, index_
8
9 deferred class
10 V_ITERATOR [G]
11
12 inherit
13 V_INPUT_STREAM [G]
14 rename
15 search as search_forth
16 redefine
17 item,
18 search_forth
19 end
20
21 ITERATION_CURSOR [G]
22 rename
23 after as off
24 redefine
25 item
26 end
27
28 feature -- Access
29
30 target: V_CONTAINER [G]
31 -- Container to iterate over.
32
33 item: G
34 -- Item at current position.
35 deferred
36 ensure then
37 definition: Result = sequence [index_]
38 end
39
40 feature -- Measurement
41
42 index: INTEGER
43 -- Current position.
44 require
45 closed: closed
46 subjects_closed: subjects.any_item.closed
47 reads (Current, subjects.any_item.ownership_domain)
48 deferred
49 ensure
50 definition: Result = index_
51 end
52
53 valid_index (i: INTEGER): BOOLEAN
54 -- Is `i' a valid position for a cursor?
55 note
56 status: functional, ghost
57 require
58 target_exists: target /= Void
59 reads (Current, target)
60 do
61 Result := 0 <= i and i <= target.bag.count + 1
62 end
63
64 feature -- Status report
65
66 before: BOOLEAN
67 -- Is current position before any position in `target'?
68 require
69 closed: closed
70 target_closed: target.closed
71 deferred
72 ensure
73 definition: Result = (index_ = 0)
74 end
75
76 after: BOOLEAN
77 -- Is current position after any position in `target'?
78 require
79 closed
80 deferred
81 ensure
82 definition: Result = (index_ = sequence.count + 1)
83 end
84
85 off: BOOLEAN
86 -- Is current position off scope?
87 do
88 check inv end
89 Result := before or after
90 ensure then
91 new_definition: Result = not sequence.domain [index_]
92 end
93
94 is_first: BOOLEAN
95 -- Is cursor at the first position?
96 require
97 closed: closed
98 target_closed: target.closed
99 reads (Current, target.ownership_domain)
100 deferred
101 ensure
102 definition: Result = (not sequence.is_empty and index_ = 1)
103 end
104
105 is_last: BOOLEAN
106 -- Is cursor at the last position?
107 require
108 closed: closed
109 target_closed: target.closed
110 reads (Current, target.ownership_domain)
111 deferred
112 ensure
113 definition: Result = (not sequence.is_empty and index_ = sequence.count)
114 end
115
116 feature -- Cursor movement
117
118 start
119 -- Go to the first position.
120 require
121 target_closed: target.closed
122 modify_model ("index_", Current)
123 deferred
124 ensure then
125 index_effect: index_ = 1
126 end
127
128 finish
129 -- Go to the last position.
130 require
131 modify_model ("index_", Current)
132 deferred
133 ensure
134 index_effect: index_ = sequence.count
135 end
136
137 forth
138 -- Go one position forward.
139 deferred
140 ensure then
141 index_effect: index_ = old index_ + 1
142 end
143
144 back
145 -- Go one position backward.
146 require
147 not_off: not off
148 modify_model ("index_", Current)
149 deferred
150 ensure
151 index_effect: index_ = old index_ - 1
152 end
153
154 go_to (i: INTEGER)
155 -- Go to position `i'.
156 note
157 explicit: wrapping
158 require
159 has_index: valid_index (i)
160 target_closed: target.closed
161 modify_model ("index_", Current)
162 local
163 j: INTEGER
164 do
165 check inv_only ("index_constraint", "target_exists", "target_bag_constraint") end
166 if i = 0 then
167 go_before
168 elseif i = target.count + 1 then
169 go_after
170 elseif i = target.count then
171 finish
172 else
173 from
174 start
175 j := 1
176 invariant
177 is_wrapped
178 sequence.domain [i]
179 j_in_bounds: 1 <= j and j <= i
180 index_counter: index_ = j
181 until
182 j = i
183 loop
184 forth
185 j := j + 1
186 end
187 end
188 ensure
189 index_effect: index_ = i
190 end
191
192 go_before
193 -- Go before any position of `target'.
194 require
195 modify_model ("index_", Current)
196 deferred
197 ensure
198 index_effect: index_ = 0
199 end
200
201 go_after
202 -- Go after any position of `target'.
203 require
204 modify_model ("index_", Current)
205 deferred
206 ensure
207 index_effect: index_ = sequence.count + 1
208 end
209
210 search_forth (v: G)
211 -- Move to the first occurrence of `v' at or after current position.
212 -- If `v' does not occur, move `after'.
213 -- (Use reference equality.)
214 note
215 explicit: wrapping
216 do
217 check inv_only ("index_constraint") end
218 if before then
219 start
220 end
221 from
222 invariant
223 index_.old_ <= index_ and index_ <= sequence.count + 1
224 not before
225 across index_.old_.max (1) |..| (index_ - 1) as i all sequence [i.item] /= v end
226 until
227 after or else item = v
228 loop
229 forth
230 variant
231 sequence.count - index_
232 end
233 check inv_only ("box_definition_empty", "box_definition_non_empty") end
234 ensure then
235 index_effect_not_found: not sequence.tail (old index_).has (v) implies index_ = sequence.count + 1
236 index_effect_found: sequence.tail (old index_).has (v) implies index_ >= old index_ and sequence [index_] = v
237 index_constraint: not sequence.interval (old index_, index_ - 1).has (v)
238 end
239
240 search_back (v: G)
241 -- Move to the last occurrence of `v' at or before current position.
242 -- If `v' does not occur, move `before'.
243 -- (Use reference equality.)
244 note
245 explicit: wrapping
246 require
247 modify_model ("index_", Current)
248 do
249 check inv_only ("index_constraint") end
250 if after then
251 finish
252 end
253 from
254 invariant
255 0 <= index_ and index_ <= index_.old_
256 not after
257 across (index_ + 1) |..| index_.old_.min (sequence.count) as i all sequence [i.item] /= v end
258 until
259 before or else item = v
260 loop
261 back
262 variant
263 index_
264 end
265 ensure
266 index_effect_not_found: not sequence.front (old index_).has (v) implies index_ = 0
267 index_effect_found: sequence.front (old index_).has (v) implies
268 (sequence [index_] = v and not sequence.interval (index_ + 1, old index_).has (v))
269 end
270
271 feature -- Specification
272
273 sequence: MML_SEQUENCE [G]
274 -- Sequence of elements in `target'.
275 note
276 status: ghost
277 attribute
278 end
279
280 index_: INTEGER
281 -- Current position.
282 note
283 status: ghost
284 replaces: box
285 attribute
286 end
287
288 invariant
289 target_exists: target /= Void
290 subjects_definition: subjects = [target]
291 target_bag_constraint: target.bag ~ sequence.to_bag
292 index_constraint: 0 <= index_ and index_ <= sequence.count + 1
293 box_definition_empty: not sequence.domain [index_] implies box.is_empty
294 box_definition_non_empty: sequence.domain [index_] implies box ~ << sequence [index_] >>
295
296 note
297 copyright: "Copyright (c) 1984-2014, Eiffel Software and others"
298 license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
299 source: "[
300 Eiffel Software
301 5949 Hollister Ave., Goleta, CA 93117 USA
302 Telephone 805-685-1006, Fax 805-685-6869
303 Website http://www.eiffel.com
304 Customer support http://support.eiffel.com
305 ]"
306 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23