-
Notifications
You must be signed in to change notification settings - Fork 2
/
v_map_iterator.e
107 lines (93 loc) · 2.55 KB
/
v_map_iterator.e
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
note
description: "Iterators to read from maps in linear order."
author: "Nadia Polikarpova"
model: target, sequence, index_
manual_inv: true
false_guards: true
deferred class
V_MAP_ITERATOR [K, 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]
modify_model ("index_", Current)
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
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)
end