/
v_hash_set.e
192 lines (164 loc) · 4.25 KB
/
v_hash_set.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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
note
description: "[
Hash sets with hash function provided by HASHABLE and object equality.
Implementation uses hash tables.
Search, extension and removal are amortized constant time.
]"
author: "Nadia Polikarpova"
model: set, lock
manual_inv: true
false_guards: true
frozen class
V_HASH_SET [G -> V_HASHABLE]
inherit
V_SET [G]
redefine
is_equal_,
lock,
forget_iterator
end
create
make
feature {NONE} -- Initialization
make (l: V_HASH_LOCK [G])
-- Create an empty set with lock `l'.
note
status: creator
require
l_wrapped: l.is_wrapped
modify (Current)
modify_model ("observers", l)
do
create table.make (l)
l.add_client (Current)
ensure then
set_empty: set.is_empty
lock_set: lock = l
observers_empty: observers.is_empty
end
feature -- Initialization
copy_ (other: V_HASH_SET [G])
-- Initialize by copying all the items of `other'.
note
explicit: wrapping
require
lock_wrapped: lock.is_wrapped
same_lock: lock = other.lock
no_iterators: observers.is_empty
modify_model ("set", Current)
modify_model ("observers", [Current, other])
do
if other /= Current then
unwrap
other.unwrap
table.copy_ (other.table)
other.wrap
wrap
end
ensure
set_effect: set ~ old other.set
observers_restored: observers ~ old observers
other_observers_restored: other.observers ~ old other.observers
end
feature -- Measurement
count: INTEGER
-- Number of elements.
do
check inv end
Result := table.count
end
feature -- Search
has (v: G): BOOLEAN
-- Is `v' contained?
-- (Uses object equality.)
do
check inv end
Result := table.has_key (v)
end
item (v: G): G
-- Element of `set' equivalent to `v' according to object equality.
do
check inv end
Result := table.key (v)
end
feature -- Iteration
new_cursor: V_HASH_SET_ITERATOR [G]
-- New iterator pointing to a position in the set, from which it can traverse all elements by going `forth'.
note
status: impure
do
create Result.make (Current)
Result.start
end
at (v: G): V_HASH_SET_ITERATOR [G]
-- New iterator over `Current' pointing at element `v' if it exists and `after' otherwise.
note
status: impure
do
create Result.make (Current)
Result.search (v)
end
feature -- Comparison
is_equal_ (other: like Current): BOOLEAN
-- Is the abstract state of Current equal to that of `other'?
do
check inv; other.inv end
check table.inv_only ("subjects_definition"); other.table.inv_only ("subjects_definition") end
Result := table.is_equal_ (other.table)
end
feature -- Extension
extend (v: G)
-- Add `v' to the set.
do
check table.inv_only ("items_locked", "locked_definition") end
check lock.inv_only ("owns_definition") end
table.force (Void, v)
check table.inv_only ("locked_definition", "no_duplicates") end
if not table.domain_has (v).old_ then
check table.map.domain [v] end
else
check table.map.domain = table.map.domain.old_ end
end
end
feature -- Removal
wipe_out
-- Remove all elements.
do
table.lemma_domain
table.wipe_out
end
feature -- Implementation
table: V_HASH_TABLE [G, ANY]
-- Hash table that stores set elements as keys.
feature -- Specification
lock: V_HASH_LOCK [G]
-- Helper object for keeping items consistent.
note
status: ghost
attribute
end
forget_iterator (it: V_ITERATOR [G])
-- Remove `it' from `observers'.
note
status: ghost
explicit: contracts
do
check it.inv_only ("subjects_definition", "A2") end
check attached {V_HASH_SET_ITERATOR [G]} it as hsit then
hsit.unwrap
set_observers (observers / hsit)
check hsit.iterator.inv_only ("subjects_definition", "A2") end
table.lemma_domain
check hsit.iterator.inv_only ("owns_definition"); hsit.iterator.list_iterator.inv_only ("default_owns") end
table.forget_iterator (hsit.iterator)
end
end
invariant
table_exists: table /= Void
owns_definition: owns = [table]
set_implementation: set = table.map.domain
table_values_definition: across set as x all table.map [x.item] = Void end
same_lock: lock = table.lock
observers_type: across observers as o all attached {V_HASH_SET_ITERATOR [G]} o.item end
observers_correspond: table.observers.count <= observers.count
end