note description: "Iterators to read from maps in linear order." author: "Nadia Polikarpova" revised_by: "Alexander Kogtenkov" model: target, sequence, index_ manual_inv: true false_guards: true deferred class V_MAP_ITERATOR [K -> ANY, V] inherit V_ITERATOR [V] rename sequence as value_sequence redefine target, is_model_equal end feature -- Access key: K -- Key at current position. require closed: closed target_closed: target.closed not_off: not off deferred ensure definition: Result = sequence [index_] end target: V_MAP [K, V] -- Table to iterate over. feature -- Cursor movement search_key (k: K) -- Move to a position where key is equivalent to `k'. -- If `k' does not appear, go after. -- (Use object equality.) require target_closed: target.closed lock_wrapped: target.lock.is_wrapped k_locked: target.lock.locked [k] deferred ensure index_effect_found: target.domain_has (k) implies sequence [index_] = target.domain_item (k) index_effect_not_found: not target.domain_has (k) implies index_ = sequence.count + 1 modify_model ("index_", Current) end feature -- Specification sequence: MML_SEQUENCE [K] -- Sequence of keys. note status: ghost replaces: value_sequence attribute end value_sequence_from (seq: like sequence; m: like target.map): MML_SEQUENCE [V] -- Value sequnce for key sequence `seq' and target map `m'. note status: ghost, functional, nonvariant, opaque, static require in_domain: seq.range <= m.domain reads ([]) do Result := m.sequence_image (seq) ensure same_count: Result.count = seq.count end is_model_equal (other: like Current): BOOLEAN -- Is iterator traversing the same container in the same order and is at the same position at `other'? note status: ghost, functional, nonvariant do Result := target = other.target and sequence = other.sequence and index_ = other.index_ end lemma_sequence_no_duplicates -- Key sequence has no duplicates. note status: lemma, nonvariant require closed: closed target_closed: target.closed do check inv end check target.inv_only ("bag_definition") end use_definition (target.bag_from (target.map)) check value_sequence.count = value_sequence.to_bag.count end check sequence.to_bag.domain = sequence.range end sequence.to_bag.lemma_domain_count sequence.lemma_no_duplicates ensure sequence.no_duplicates end invariant target_domain_constraint: target.map.domain ~ sequence.range value_sequence_definition: value_sequence ~ value_sequence_from (sequence, target.map) note copyright: "Copyright (c) 1984-2018, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end