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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94603 - (show annotations)
Fri Mar 14 18:21:48 2014 UTC (5 years, 9 months ago) by polikarn
File size: 1447 byte(s)
Removed global_public (super slow) and added annotations as a consequence; reseting type/var counters after every verification; changed EB2 specs to verify with the sound invariant frame axiom.
1 note
2 description: "Itreators to read from sequences."
3 author: "Nadia Polikarpova"
4 model: target, index_
5
6 deferred class
7 V_SEQUENCE_ITERATOR [G]
8
9 inherit
10 V_MAP_ITERATOR [INTEGER, G]
11 rename
12 key as target_index,
13 search_key as search_target_index,
14 key_sequence as target_index_sequence,
15 value_sequence as sequence
16 redefine
17 target
18 end
19
20 feature -- Access
21
22 target_index: INTEGER
23 -- Target index at current position.
24 do
25 check inv end
26 Result := target.lower + index_ - 1
27 end
28
29 target: V_SEQUENCE [G]
30 -- Sequence to iterate over.
31
32 feature -- Cursor movement
33
34 search_target_index (i: INTEGER)
35 -- Move to a position where target index is `i'.
36 -- If `i' is not a valid index, go after.
37 -- (Use reference equlity.)
38 note
39 explicit: wrapping
40 do
41 check inv end
42 check target.inv end
43 if target.has_index (i) then
44 go_to (i - target.lower + 1)
45 else
46 go_after
47 end
48 end
49
50 invariant
51 target_index_sequence_definition: across target_index_sequence.domain as i all target_index_sequence [i.item] = target.lower_ + i.item - 1 end
52
53 note
54 copyright: "Copyright (c) 1984-2014, Eiffel Software and others"
55 license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
56 source: "[
57 Eiffel Software
58 5949 Hollister Ave., Goleta, CA 93117 USA
59 Telephone 805-685-1006, Fax 805-685-6869
60 Website http://www.eiffel.com
61 Customer support http://support.eiffel.com
62 ]"
63 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23