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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94603 - (show annotations)
Fri Mar 14 18:21:48 2014 UTC (5 years, 8 months ago) by polikarn
File size: 1823 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: "Iterators to read from maps in linear order."
3 author: "Nadia Polikarpova"
4 model: target, key_sequence, index_
5
6 deferred class
7 V_MAP_ITERATOR [K, V]
8
9 inherit
10 V_ITERATOR [V]
11 rename
12 sequence as value_sequence
13 redefine
14 target
15 end
16
17 feature -- Access
18
19 key: K
20 -- Key at current position.
21 require
22 closed: closed
23 target_closed: target.closed
24 not_off: not off
25 reads (Current, target)
26 deferred
27 ensure
28 definition: Result = key_sequence [index_]
29 end
30
31 target: V_MAP [K, V]
32 -- Map to iterate over.
33
34 feature -- Cursor movement
35
36 search_key (k: K)
37 -- Move to a position where key is equal to `k'.
38 -- If `k' does not appear, go after.
39 -- (Use reference equality.)
40 require
41 modify_model ("index_", Current)
42 target.is_wrapped
43 deferred
44 ensure
45 index_effect_found: target.has_key (k) implies key_sequence [index_] = k
46 index_effect_not_found: not target.has_key (k) implies index_ = key_sequence.count + 1
47 end
48
49 feature -- Specification
50
51 key_sequence: MML_SEQUENCE [K]
52 -- Sequence of keys.
53 note
54 status: ghost
55 replaces: value_sequence
56 attribute
57 end
58
59 invariant
60 keys_in_target: key_sequence.range ~ target.map.domain
61 unique_keys: key_sequence.count = target.map.count
62 value_sequence_domain_definition: value_sequence.count = key_sequence.count
63 value_sequence_definition: across key_sequence.domain as i all value_sequence [i.item] = target.map [key_sequence [i.item]] end
64
65 note
66 copyright: "Copyright (c) 1984-2014, Eiffel Software and others"
67 license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
68 source: "[
69 Eiffel Software
70 5949 Hollister Ave., Goleta, CA 93117 USA
71 Telephone 805-685-1006, Fax 805-685-6869
72 Website http://www.eiffel.com
73 Customer support http://support.eiffel.com
74 ]"
75 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23