|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2004-2019, Free Software Foundation, Inc. --
|
|
111
|
10 -- --
|
|
|
11 -- This specification is derived from the Ada Reference Manual for use with --
|
|
|
12 -- GNAT. The copyright notice above, and the license provisions that follow --
|
|
|
13 -- apply solely to the contents of the part following the private keyword. --
|
|
|
14 -- --
|
|
|
15 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
16 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
|
|
|
21 -- --
|
|
|
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
23 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
24 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
25 -- --
|
|
|
26 -- You should have received a copy of the GNU General Public License and --
|
|
|
27 -- a copy of the GCC Runtime Library Exception along with this program; --
|
|
|
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
|
|
29 -- <http://www.gnu.org/licenses/>. --
|
|
|
30 ------------------------------------------------------------------------------
|
|
|
31
|
|
|
32 -- This spec is derived from package Ada.Containers.Bounded_Hashed_Maps in the
|
|
|
33 -- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
|
|
|
34 -- making it easier to express properties, and by making the specification of
|
|
|
35 -- this unit compatible with SPARK 2014. Note that the API of this unit may be
|
|
|
36 -- subject to incompatible changes as SPARK 2014 evolves.
|
|
|
37
|
|
|
38 -- The modifications are:
|
|
|
39
|
|
|
40 -- A parameter for the container is added to every function reading the
|
|
|
41 -- contents of a container: Key, Element, Next, Query_Element, Has_Element,
|
|
|
42 -- Iterate, Equivalent_Keys. This change is motivated by the need to have
|
|
|
43 -- cursors which are valid on different containers (typically a container C
|
|
|
44 -- and its previous version C'Old) for expressing properties, which is not
|
|
|
45 -- possible if cursors encapsulate an access to the underlying container.
|
|
|
46
|
|
|
47 -- Iteration over maps is done using the Iterable aspect, which is SPARK
|
|
|
48 -- compatible. "For of" iteration ranges over keys instead of elements.
|
|
|
49
|
|
|
50 with Ada.Containers.Functional_Vectors;
|
|
|
51 with Ada.Containers.Functional_Maps;
|
|
|
52 private with Ada.Containers.Hash_Tables;
|
|
|
53
|
|
|
54 generic
|
|
|
55 type Key_Type is private;
|
|
|
56 type Element_Type is private;
|
|
|
57
|
|
|
58 with function Hash (Key : Key_Type) return Hash_Type;
|
|
|
59 with function Equivalent_Keys
|
|
|
60 (Left : Key_Type;
|
|
|
61 Right : Key_Type) return Boolean is "=";
|
|
145
|
62 with function "=" (Left, Right : Element_Type) return Boolean is <>;
|
|
111
|
63
|
|
|
64 package Ada.Containers.Formal_Hashed_Maps with
|
|
|
65 SPARK_Mode
|
|
|
66 is
|
|
|
67 pragma Annotate (CodePeer, Skip_Analysis);
|
|
|
68
|
|
|
69 type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
|
|
|
70 Iterable => (First => First,
|
|
|
71 Next => Next,
|
|
|
72 Has_Element => Has_Element,
|
|
|
73 Element => Key),
|
|
|
74 Default_Initial_Condition => Is_Empty (Map);
|
|
|
75 pragma Preelaborable_Initialization (Map);
|
|
|
76
|
|
|
77 Empty_Map : constant Map;
|
|
|
78
|
|
|
79 type Cursor is record
|
|
|
80 Node : Count_Type;
|
|
|
81 end record;
|
|
|
82
|
|
|
83 No_Element : constant Cursor := (Node => 0);
|
|
|
84
|
|
|
85 function Length (Container : Map) return Count_Type with
|
|
|
86 Global => null,
|
|
|
87 Post => Length'Result <= Container.Capacity;
|
|
|
88
|
|
|
89 pragma Unevaluated_Use_Of_Old (Allow);
|
|
|
90
|
|
|
91 package Formal_Model with Ghost is
|
|
|
92 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
|
|
|
93
|
|
|
94 package M is new Ada.Containers.Functional_Maps
|
|
|
95 (Element_Type => Element_Type,
|
|
|
96 Key_Type => Key_Type,
|
|
|
97 Equivalent_Keys => Equivalent_Keys);
|
|
|
98
|
|
|
99 function "="
|
|
|
100 (Left : M.Map;
|
|
|
101 Right : M.Map) return Boolean renames M."=";
|
|
|
102
|
|
|
103 function "<="
|
|
|
104 (Left : M.Map;
|
|
|
105 Right : M.Map) return Boolean renames M."<=";
|
|
|
106
|
|
|
107 package K is new Ada.Containers.Functional_Vectors
|
|
|
108 (Element_Type => Key_Type,
|
|
|
109 Index_Type => Positive_Count_Type);
|
|
|
110
|
|
|
111 function "="
|
|
|
112 (Left : K.Sequence;
|
|
|
113 Right : K.Sequence) return Boolean renames K."=";
|
|
|
114
|
|
|
115 function "<"
|
|
|
116 (Left : K.Sequence;
|
|
|
117 Right : K.Sequence) return Boolean renames K."<";
|
|
|
118
|
|
|
119 function "<="
|
|
|
120 (Left : K.Sequence;
|
|
|
121 Right : K.Sequence) return Boolean renames K."<=";
|
|
|
122
|
|
|
123 function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
|
|
|
124 -- Search for Key in Container
|
|
|
125
|
|
|
126 with
|
|
|
127 Global => null,
|
|
|
128 Post =>
|
|
|
129 (if Find'Result > 0 then
|
|
|
130 Find'Result <= K.Length (Container)
|
|
|
131 and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
|
|
|
132
|
|
|
133 function K_Keys_Included
|
|
|
134 (Left : K.Sequence;
|
|
|
135 Right : K.Sequence) return Boolean
|
|
|
136 -- Return True if Right contains all the keys of Left
|
|
|
137
|
|
|
138 with
|
|
|
139 Global => null,
|
|
|
140 Post =>
|
|
|
141 K_Keys_Included'Result =
|
|
|
142 (for all I in 1 .. K.Length (Left) =>
|
|
|
143 Find (Right, K.Get (Left, I)) > 0
|
|
|
144 and then K.Get (Right, Find (Right, K.Get (Left, I))) =
|
|
|
145 K.Get (Left, I));
|
|
|
146
|
|
|
147 package P is new Ada.Containers.Functional_Maps
|
|
|
148 (Key_Type => Cursor,
|
|
|
149 Element_Type => Positive_Count_Type,
|
|
|
150 Equivalent_Keys => "=",
|
|
|
151 Enable_Handling_Of_Equivalence => False);
|
|
|
152
|
|
|
153 function "="
|
|
|
154 (Left : P.Map;
|
|
|
155 Right : P.Map) return Boolean renames P."=";
|
|
|
156
|
|
|
157 function "<="
|
|
|
158 (Left : P.Map;
|
|
|
159 Right : P.Map) return Boolean renames P."<=";
|
|
|
160
|
|
|
161 function Mapping_Preserved
|
|
|
162 (K_Left : K.Sequence;
|
|
|
163 K_Right : K.Sequence;
|
|
|
164 P_Left : P.Map;
|
|
|
165 P_Right : P.Map) return Boolean
|
|
|
166 with
|
|
|
167 Global => null,
|
|
|
168 Post =>
|
|
|
169 (if Mapping_Preserved'Result then
|
|
|
170
|
|
|
171 -- Right contains all the cursors of Left
|
|
|
172
|
|
|
173 P.Keys_Included (P_Left, P_Right)
|
|
|
174
|
|
|
175 -- Right contains all the keys of Left
|
|
|
176
|
|
|
177 and K_Keys_Included (K_Left, K_Right)
|
|
|
178
|
|
|
179 -- Mappings from cursors to elements induced by K_Left, P_Left
|
|
|
180 -- and K_Right, P_Right are the same.
|
|
|
181
|
|
|
182 and (for all C of P_Left =>
|
|
|
183 K.Get (K_Left, P.Get (P_Left, C)) =
|
|
|
184 K.Get (K_Right, P.Get (P_Right, C))));
|
|
|
185
|
|
|
186 function Model (Container : Map) return M.Map with
|
|
|
187 -- The high-level model of a map is a map from keys to elements. Neither
|
|
|
188 -- cursors nor order of elements are represented in this model. Keys are
|
|
|
189 -- modeled up to equivalence.
|
|
|
190
|
|
|
191 Ghost,
|
|
|
192 Global => null;
|
|
|
193
|
|
|
194 function Keys (Container : Map) return K.Sequence with
|
|
|
195 -- The Keys sequence represents the underlying list structure of maps
|
|
|
196 -- that is used for iteration. It stores the actual values of keys in
|
|
|
197 -- the map. It does not model cursors nor elements.
|
|
|
198
|
|
|
199 Ghost,
|
|
|
200 Global => null,
|
|
|
201 Post =>
|
|
|
202 K.Length (Keys'Result) = Length (Container)
|
|
|
203
|
|
|
204 -- It only contains keys contained in Model
|
|
|
205
|
|
|
206 and (for all Key of Keys'Result =>
|
|
|
207 M.Has_Key (Model (Container), Key))
|
|
|
208
|
|
|
209 -- It contains all the keys contained in Model
|
|
|
210
|
|
|
211 and (for all Key of Model (Container) =>
|
|
|
212 (Find (Keys'Result, Key) > 0
|
|
|
213 and then Equivalent_Keys
|
|
|
214 (K.Get (Keys'Result, Find (Keys'Result, Key)),
|
|
|
215 Key)))
|
|
|
216
|
|
|
217 -- It has no duplicate
|
|
|
218
|
|
|
219 and (for all I in 1 .. Length (Container) =>
|
|
|
220 Find (Keys'Result, K.Get (Keys'Result, I)) = I)
|
|
|
221
|
|
|
222 and (for all I in 1 .. Length (Container) =>
|
|
|
223 (for all J in 1 .. Length (Container) =>
|
|
|
224 (if Equivalent_Keys
|
|
|
225 (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
|
|
|
226 then
|
|
|
227 I = J)));
|
|
|
228 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
|
|
|
229
|
|
|
230 function Positions (Container : Map) return P.Map with
|
|
|
231 -- The Positions map is used to model cursors. It only contains valid
|
|
|
232 -- cursors and maps them to their position in the container.
|
|
|
233
|
|
|
234 Ghost,
|
|
|
235 Global => null,
|
|
|
236 Post =>
|
|
|
237 not P.Has_Key (Positions'Result, No_Element)
|
|
|
238
|
|
|
239 -- Positions of cursors are smaller than the container's length
|
|
|
240
|
|
|
241 and then
|
|
|
242 (for all I of Positions'Result =>
|
|
|
243 P.Get (Positions'Result, I) in 1 .. Length (Container)
|
|
|
244
|
|
|
245 -- No two cursors have the same position. Note that we do not
|
|
|
246 -- state that there is a cursor in the map for each position, as
|
|
|
247 -- it is rarely needed.
|
|
|
248
|
|
|
249 and then
|
|
|
250 (for all J of Positions'Result =>
|
|
|
251 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
|
|
|
252 then I = J)));
|
|
|
253
|
|
|
254 procedure Lift_Abstraction_Level (Container : Map) with
|
|
|
255 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
|
|
|
256 -- assume that we can access the same elements by iterating over
|
|
|
257 -- positions or cursors.
|
|
|
258 -- This information is not generally useful except when switching from
|
|
|
259 -- a low-level, cursor-aware view of a container, to a high-level,
|
|
|
260 -- position-based view.
|
|
|
261
|
|
|
262 Ghost,
|
|
|
263 Global => null,
|
|
|
264 Post =>
|
|
|
265 (for all Key of Keys (Container) =>
|
|
|
266 (for some I of Positions (Container) =>
|
|
|
267 K.Get (Keys (Container), P.Get (Positions (Container), I)) =
|
|
|
268 Key));
|
|
|
269
|
|
|
270 function Contains
|
|
|
271 (C : M.Map;
|
|
|
272 K : Key_Type) return Boolean renames M.Has_Key;
|
|
|
273 -- To improve readability of contracts, we rename the function used to
|
|
|
274 -- search for a key in the model to Contains.
|
|
|
275
|
|
|
276 function Element
|
|
|
277 (C : M.Map;
|
|
|
278 K : Key_Type) return Element_Type renames M.Get;
|
|
|
279 -- To improve readability of contracts, we rename the function used to
|
|
|
280 -- access an element in the model to Element.
|
|
|
281
|
|
|
282 end Formal_Model;
|
|
|
283 use Formal_Model;
|
|
|
284
|
|
|
285 function "=" (Left, Right : Map) return Boolean with
|
|
|
286 Global => null,
|
|
|
287 Post => "="'Result = (Model (Left) = Model (Right));
|
|
|
288
|
|
|
289 function Capacity (Container : Map) return Count_Type with
|
|
|
290 Global => null,
|
|
|
291 Post => Capacity'Result = Container.Capacity;
|
|
|
292
|
|
|
293 procedure Reserve_Capacity
|
|
|
294 (Container : in out Map;
|
|
|
295 Capacity : Count_Type)
|
|
|
296 with
|
|
|
297 Global => null,
|
|
|
298 Pre => Capacity <= Container.Capacity,
|
|
|
299 Post =>
|
|
|
300 Model (Container) = Model (Container)'Old
|
|
|
301 and Length (Container)'Old = Length (Container)
|
|
|
302
|
|
|
303 -- Actual keys are preserved
|
|
|
304
|
|
|
305 and K_Keys_Included (Keys (Container), Keys (Container)'Old)
|
|
|
306 and K_Keys_Included (Keys (Container)'Old, Keys (Container));
|
|
|
307
|
|
|
308 function Is_Empty (Container : Map) return Boolean with
|
|
|
309 Global => null,
|
|
|
310 Post => Is_Empty'Result = (Length (Container) = 0);
|
|
|
311
|
|
|
312 procedure Clear (Container : in out Map) with
|
|
|
313 Global => null,
|
|
|
314 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
|
|
|
315
|
|
|
316 procedure Assign (Target : in out Map; Source : Map) with
|
|
|
317 Global => null,
|
|
|
318 Pre => Target.Capacity >= Length (Source),
|
|
|
319 Post =>
|
|
|
320 Model (Target) = Model (Source)
|
|
|
321 and Length (Source) = Length (Target)
|
|
|
322
|
|
|
323 -- Actual keys are preserved
|
|
|
324
|
|
|
325 and K_Keys_Included (Keys (Target), Keys (Source))
|
|
|
326 and K_Keys_Included (Keys (Source), Keys (Target));
|
|
|
327
|
|
|
328 function Copy
|
|
|
329 (Source : Map;
|
|
|
330 Capacity : Count_Type := 0) return Map
|
|
|
331 with
|
|
|
332 Global => null,
|
|
|
333 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
|
|
|
334 Post =>
|
|
|
335 Model (Copy'Result) = Model (Source)
|
|
|
336 and Keys (Copy'Result) = Keys (Source)
|
|
|
337 and Positions (Copy'Result) = Positions (Source)
|
|
|
338 and (if Capacity = 0 then
|
|
|
339 Copy'Result.Capacity = Source.Capacity
|
|
|
340 else
|
|
|
341 Copy'Result.Capacity = Capacity);
|
|
|
342 -- Copy returns a container stricty equal to Source. It must have the same
|
|
|
343 -- cursors associated with each element. Therefore:
|
|
|
344 -- - capacity=0 means use Source.Capacity as capacity of target
|
|
|
345 -- - the modulus cannot be changed.
|
|
|
346
|
|
|
347 function Key (Container : Map; Position : Cursor) return Key_Type with
|
|
|
348 Global => null,
|
|
|
349 Pre => Has_Element (Container, Position),
|
|
|
350 Post =>
|
|
|
351 Key'Result =
|
|
|
352 K.Get (Keys (Container), P.Get (Positions (Container), Position));
|
|
|
353 pragma Annotate (GNATprove, Inline_For_Proof, Key);
|
|
|
354
|
|
|
355 function Element
|
|
|
356 (Container : Map;
|
|
|
357 Position : Cursor) return Element_Type
|
|
|
358 with
|
|
|
359 Global => null,
|
|
|
360 Pre => Has_Element (Container, Position),
|
|
|
361 Post =>
|
|
|
362 Element'Result = Element (Model (Container), Key (Container, Position));
|
|
|
363 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
364
|
|
|
365 procedure Replace_Element
|
|
|
366 (Container : in out Map;
|
|
|
367 Position : Cursor;
|
|
|
368 New_Item : Element_Type)
|
|
|
369 with
|
|
|
370 Global => null,
|
|
|
371 Pre => Has_Element (Container, Position),
|
|
|
372 Post =>
|
|
|
373
|
|
|
374 -- Order of keys and cursors is preserved
|
|
|
375
|
|
|
376 Keys (Container) = Keys (Container)'Old
|
|
|
377 and Positions (Container) = Positions (Container)'Old
|
|
|
378
|
|
|
379 -- New_Item is now associated with the key at position Position in
|
|
|
380 -- Container.
|
|
|
381
|
|
|
382 and Element (Container, Position) = New_Item
|
|
|
383
|
|
|
384 -- Elements associated with other keys are preserved
|
|
|
385
|
|
|
386 and M.Same_Keys (Model (Container), Model (Container)'Old)
|
|
|
387 and M.Elements_Equal_Except
|
|
|
388 (Model (Container),
|
|
|
389 Model (Container)'Old,
|
|
|
390 Key (Container, Position));
|
|
|
391
|
|
|
392 procedure Move (Target : in out Map; Source : in out Map) with
|
|
|
393 Global => null,
|
|
|
394 Pre => Target.Capacity >= Length (Source),
|
|
|
395 Post =>
|
|
|
396 Model (Target) = Model (Source)'Old
|
|
|
397 and Length (Source)'Old = Length (Target)
|
|
|
398 and Length (Source) = 0
|
|
|
399
|
|
|
400 -- Actual keys are preserved
|
|
|
401
|
|
|
402 and K_Keys_Included (Keys (Target), Keys (Source)'Old)
|
|
|
403 and K_Keys_Included (Keys (Source)'Old, Keys (Target));
|
|
|
404
|
|
|
405 procedure Insert
|
|
|
406 (Container : in out Map;
|
|
|
407 Key : Key_Type;
|
|
|
408 New_Item : Element_Type;
|
|
|
409 Position : out Cursor;
|
|
|
410 Inserted : out Boolean)
|
|
|
411 with
|
|
|
412 Global => null,
|
|
|
413 Pre =>
|
|
|
414 Length (Container) < Container.Capacity or Contains (Container, Key),
|
|
|
415 Post =>
|
|
|
416 Contains (Container, Key)
|
|
|
417 and Has_Element (Container, Position)
|
|
|
418 and Equivalent_Keys
|
|
|
419 (Formal_Hashed_Maps.Key (Container, Position), Key),
|
|
|
420 Contract_Cases =>
|
|
|
421
|
|
|
422 -- If Key is already in Container, it is not modified and Inserted is
|
|
|
423 -- set to False.
|
|
|
424
|
|
|
425 (Contains (Container, Key) =>
|
|
|
426 not Inserted
|
|
|
427 and Model (Container) = Model (Container)'Old
|
|
|
428 and Keys (Container) = Keys (Container)'Old
|
|
|
429 and Positions (Container) = Positions (Container)'Old,
|
|
|
430
|
|
|
431 -- Otherwise, Key is inserted in Container and Inserted is set to True
|
|
|
432
|
|
|
433 others =>
|
|
|
434 Inserted
|
|
|
435 and Length (Container) = Length (Container)'Old + 1
|
|
|
436
|
|
|
437 -- Key now maps to New_Item
|
|
|
438
|
|
|
439 and Formal_Hashed_Maps.Key (Container, Position) = Key
|
|
|
440 and Element (Model (Container), Key) = New_Item
|
|
|
441
|
|
|
442 -- Other keys are preserved
|
|
|
443
|
|
|
444 and Model (Container)'Old <= Model (Container)
|
|
|
445 and M.Keys_Included_Except
|
|
|
446 (Model (Container),
|
|
|
447 Model (Container)'Old,
|
|
|
448 Key)
|
|
|
449
|
|
|
450 -- Mapping from cursors to keys is preserved
|
|
|
451
|
|
|
452 and Mapping_Preserved
|
|
|
453 (K_Left => Keys (Container)'Old,
|
|
|
454 K_Right => Keys (Container),
|
|
|
455 P_Left => Positions (Container)'Old,
|
|
|
456 P_Right => Positions (Container))
|
|
|
457 and P.Keys_Included_Except
|
|
|
458 (Positions (Container),
|
|
|
459 Positions (Container)'Old,
|
|
|
460 Position));
|
|
|
461
|
|
|
462 procedure Insert
|
|
|
463 (Container : in out Map;
|
|
|
464 Key : Key_Type;
|
|
|
465 New_Item : Element_Type)
|
|
|
466 with
|
|
|
467 Global => null,
|
|
|
468 Pre =>
|
|
|
469 Length (Container) < Container.Capacity
|
|
|
470 and then (not Contains (Container, Key)),
|
|
|
471 Post =>
|
|
|
472 Length (Container) = Length (Container)'Old + 1
|
|
|
473 and Contains (Container, Key)
|
|
|
474
|
|
|
475 -- Key now maps to New_Item
|
|
|
476
|
|
|
477 and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
|
|
|
478 and Element (Model (Container), Key) = New_Item
|
|
|
479
|
|
|
480 -- Other keys are preserved
|
|
|
481
|
|
|
482 and Model (Container)'Old <= Model (Container)
|
|
|
483 and M.Keys_Included_Except
|
|
|
484 (Model (Container),
|
|
|
485 Model (Container)'Old,
|
|
|
486 Key)
|
|
|
487
|
|
|
488 -- Mapping from cursors to keys is preserved
|
|
|
489
|
|
|
490 and Mapping_Preserved
|
|
|
491 (K_Left => Keys (Container)'Old,
|
|
|
492 K_Right => Keys (Container),
|
|
|
493 P_Left => Positions (Container)'Old,
|
|
|
494 P_Right => Positions (Container))
|
|
|
495 and P.Keys_Included_Except
|
|
|
496 (Positions (Container),
|
|
|
497 Positions (Container)'Old,
|
|
|
498 Find (Container, Key));
|
|
|
499
|
|
|
500 procedure Include
|
|
|
501 (Container : in out Map;
|
|
|
502 Key : Key_Type;
|
|
|
503 New_Item : Element_Type)
|
|
|
504 with
|
|
|
505 Global => null,
|
|
|
506 Pre =>
|
|
|
507 Length (Container) < Container.Capacity or Contains (Container, Key),
|
|
|
508 Post =>
|
|
|
509 Contains (Container, Key) and Element (Container, Key) = New_Item,
|
|
|
510 Contract_Cases =>
|
|
|
511
|
|
|
512 -- If Key is already in Container, Key is mapped to New_Item
|
|
|
513
|
|
|
514 (Contains (Container, Key) =>
|
|
|
515
|
|
|
516 -- Cursors are preserved
|
|
|
517
|
|
|
518 Positions (Container) = Positions (Container)'Old
|
|
|
519
|
|
|
520 -- The key equivalent to Key in Container is replaced by Key
|
|
|
521
|
|
|
522 and K.Get
|
|
|
523 (Keys (Container),
|
|
|
524 P.Get (Positions (Container), Find (Container, Key))) = Key
|
|
|
525 and K.Equal_Except
|
|
|
526 (Keys (Container)'Old,
|
|
|
527 Keys (Container),
|
|
|
528 P.Get (Positions (Container), Find (Container, Key)))
|
|
|
529
|
|
|
530 -- Elements associated with other keys are preserved
|
|
|
531
|
|
|
532 and M.Same_Keys (Model (Container), Model (Container)'Old)
|
|
|
533 and M.Elements_Equal_Except
|
|
|
534 (Model (Container),
|
|
|
535 Model (Container)'Old,
|
|
|
536 Key),
|
|
|
537
|
|
|
538 -- Otherwise, Key is inserted in Container
|
|
|
539
|
|
|
540 others =>
|
|
|
541 Length (Container) = Length (Container)'Old + 1
|
|
|
542
|
|
|
543 -- Other keys are preserved
|
|
|
544
|
|
|
545 and Model (Container)'Old <= Model (Container)
|
|
|
546 and M.Keys_Included_Except
|
|
|
547 (Model (Container),
|
|
|
548 Model (Container)'Old,
|
|
|
549 Key)
|
|
|
550
|
|
|
551 -- Key is inserted in Container
|
|
|
552
|
|
|
553 and K.Get
|
|
|
554 (Keys (Container),
|
|
|
555 P.Get (Positions (Container), Find (Container, Key))) = Key
|
|
|
556
|
|
|
557 -- Mapping from cursors to keys is preserved
|
|
|
558
|
|
|
559 and Mapping_Preserved
|
|
|
560 (K_Left => Keys (Container)'Old,
|
|
|
561 K_Right => Keys (Container),
|
|
|
562 P_Left => Positions (Container)'Old,
|
|
|
563 P_Right => Positions (Container))
|
|
|
564 and P.Keys_Included_Except
|
|
|
565 (Positions (Container),
|
|
|
566 Positions (Container)'Old,
|
|
|
567 Find (Container, Key)));
|
|
|
568
|
|
|
569 procedure Replace
|
|
|
570 (Container : in out Map;
|
|
|
571 Key : Key_Type;
|
|
|
572 New_Item : Element_Type)
|
|
|
573 with
|
|
|
574 Global => null,
|
|
|
575 Pre => Contains (Container, Key),
|
|
|
576 Post =>
|
|
|
577
|
|
|
578 -- Cursors are preserved
|
|
|
579
|
|
|
580 Positions (Container) = Positions (Container)'Old
|
|
|
581
|
|
|
582 -- The key equivalent to Key in Container is replaced by Key
|
|
|
583
|
|
|
584 and K.Get
|
|
|
585 (Keys (Container),
|
|
|
586 P.Get (Positions (Container), Find (Container, Key))) = Key
|
|
|
587 and K.Equal_Except
|
|
|
588 (Keys (Container)'Old,
|
|
|
589 Keys (Container),
|
|
|
590 P.Get (Positions (Container), Find (Container, Key)))
|
|
|
591
|
|
|
592 -- New_Item is now associated with the Key in Container
|
|
|
593
|
|
|
594 and Element (Model (Container), Key) = New_Item
|
|
|
595
|
|
|
596 -- Elements associated with other keys are preserved
|
|
|
597
|
|
|
598 and M.Same_Keys (Model (Container), Model (Container)'Old)
|
|
|
599 and M.Elements_Equal_Except
|
|
|
600 (Model (Container),
|
|
|
601 Model (Container)'Old,
|
|
|
602 Key);
|
|
|
603
|
|
|
604 procedure Exclude (Container : in out Map; Key : Key_Type) with
|
|
|
605 Global => null,
|
|
|
606 Post => not Contains (Container, Key),
|
|
|
607 Contract_Cases =>
|
|
|
608
|
|
|
609 -- If Key is not in Container, nothing is changed
|
|
|
610
|
|
|
611 (not Contains (Container, Key) =>
|
|
|
612 Model (Container) = Model (Container)'Old
|
|
|
613 and Keys (Container) = Keys (Container)'Old
|
|
|
614 and Positions (Container) = Positions (Container)'Old,
|
|
|
615
|
|
|
616 -- Otherwise, Key is removed from Container
|
|
|
617
|
|
|
618 others =>
|
|
|
619 Length (Container) = Length (Container)'Old - 1
|
|
|
620
|
|
|
621 -- Other keys are preserved
|
|
|
622
|
|
|
623 and Model (Container) <= Model (Container)'Old
|
|
|
624 and M.Keys_Included_Except
|
|
|
625 (Model (Container)'Old,
|
|
|
626 Model (Container),
|
|
|
627 Key)
|
|
|
628
|
|
|
629 -- Mapping from cursors to keys is preserved
|
|
|
630
|
|
|
631 and Mapping_Preserved
|
|
|
632 (K_Left => Keys (Container),
|
|
|
633 K_Right => Keys (Container)'Old,
|
|
|
634 P_Left => Positions (Container),
|
|
|
635 P_Right => Positions (Container)'Old)
|
|
|
636 and P.Keys_Included_Except
|
|
|
637 (Positions (Container)'Old,
|
|
|
638 Positions (Container),
|
|
|
639 Find (Container, Key)'Old));
|
|
|
640
|
|
|
641 procedure Delete (Container : in out Map; Key : Key_Type) with
|
|
|
642 Global => null,
|
|
|
643 Pre => Contains (Container, Key),
|
|
|
644 Post =>
|
|
|
645 Length (Container) = Length (Container)'Old - 1
|
|
|
646
|
|
|
647 -- Key is no longer in Container
|
|
|
648
|
|
|
649 and not Contains (Container, Key)
|
|
|
650
|
|
|
651 -- Other keys are preserved
|
|
|
652
|
|
|
653 and Model (Container) <= Model (Container)'Old
|
|
|
654 and M.Keys_Included_Except
|
|
|
655 (Model (Container)'Old,
|
|
|
656 Model (Container),
|
|
|
657 Key)
|
|
|
658
|
|
|
659 -- Mapping from cursors to keys is preserved
|
|
|
660
|
|
|
661 and Mapping_Preserved
|
|
|
662 (K_Left => Keys (Container),
|
|
|
663 K_Right => Keys (Container)'Old,
|
|
|
664 P_Left => Positions (Container),
|
|
|
665 P_Right => Positions (Container)'Old)
|
|
|
666 and P.Keys_Included_Except
|
|
|
667 (Positions (Container)'Old,
|
|
|
668 Positions (Container),
|
|
|
669 Find (Container, Key)'Old);
|
|
|
670
|
|
|
671 procedure Delete (Container : in out Map; Position : in out Cursor) with
|
|
|
672 Global => null,
|
|
|
673 Pre => Has_Element (Container, Position),
|
|
|
674 Post =>
|
|
|
675 Position = No_Element
|
|
|
676 and Length (Container) = Length (Container)'Old - 1
|
|
|
677
|
|
|
678 -- The key at position Position is no longer in Container
|
|
|
679
|
|
|
680 and not Contains (Container, Key (Container, Position)'Old)
|
|
|
681 and not P.Has_Key (Positions (Container), Position'Old)
|
|
|
682
|
|
|
683 -- Other keys are preserved
|
|
|
684
|
|
|
685 and Model (Container) <= Model (Container)'Old
|
|
|
686 and M.Keys_Included_Except
|
|
|
687 (Model (Container)'Old,
|
|
|
688 Model (Container),
|
|
|
689 Key (Container, Position)'Old)
|
|
|
690
|
|
|
691 -- Mapping from cursors to keys is preserved
|
|
|
692
|
|
|
693 and Mapping_Preserved
|
|
|
694 (K_Left => Keys (Container),
|
|
|
695 K_Right => Keys (Container)'Old,
|
|
|
696 P_Left => Positions (Container),
|
|
|
697 P_Right => Positions (Container)'Old)
|
|
|
698 and P.Keys_Included_Except
|
|
|
699 (Positions (Container)'Old,
|
|
|
700 Positions (Container),
|
|
|
701 Position'Old);
|
|
|
702
|
|
|
703 function First (Container : Map) return Cursor with
|
|
|
704 Global => null,
|
|
|
705 Contract_Cases =>
|
|
|
706 (Length (Container) = 0 =>
|
|
|
707 First'Result = No_Element,
|
|
|
708
|
|
|
709 others =>
|
|
|
710 Has_Element (Container, First'Result)
|
|
|
711 and P.Get (Positions (Container), First'Result) = 1);
|
|
|
712
|
|
|
713 function Next (Container : Map; Position : Cursor) return Cursor with
|
|
|
714 Global => null,
|
|
|
715 Pre =>
|
|
|
716 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
717 Contract_Cases =>
|
|
|
718 (Position = No_Element
|
|
|
719 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
720 =>
|
|
|
721 Next'Result = No_Element,
|
|
|
722
|
|
|
723 others =>
|
|
|
724 Has_Element (Container, Next'Result)
|
|
|
725 and then P.Get (Positions (Container), Next'Result) =
|
|
|
726 P.Get (Positions (Container), Position) + 1);
|
|
|
727
|
|
|
728 procedure Next (Container : Map; Position : in out Cursor) with
|
|
|
729 Global => null,
|
|
|
730 Pre =>
|
|
|
731 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
732 Contract_Cases =>
|
|
|
733 (Position = No_Element
|
|
|
734 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
735 =>
|
|
|
736 Position = No_Element,
|
|
|
737
|
|
|
738 others =>
|
|
|
739 Has_Element (Container, Position)
|
|
|
740 and then P.Get (Positions (Container), Position) =
|
|
|
741 P.Get (Positions (Container), Position'Old) + 1);
|
|
|
742
|
|
|
743 function Find (Container : Map; Key : Key_Type) return Cursor with
|
|
|
744 Global => null,
|
|
|
745 Contract_Cases =>
|
|
|
746
|
|
|
747 -- If Key is not contained in Container, Find returns No_Element
|
|
|
748
|
|
|
749 (not Contains (Model (Container), Key) =>
|
|
|
750 Find'Result = No_Element,
|
|
|
751
|
|
|
752 -- Otherwise, Find returns a valid cursor in Container
|
|
|
753
|
|
|
754 others =>
|
|
|
755 P.Has_Key (Positions (Container), Find'Result)
|
|
|
756 and P.Get (Positions (Container), Find'Result) =
|
|
|
757 Find (Keys (Container), Key)
|
|
|
758
|
|
|
759 -- The key designated by the result of Find is Key
|
|
|
760
|
|
|
761 and Equivalent_Keys
|
|
|
762 (Formal_Hashed_Maps.Key (Container, Find'Result), Key));
|
|
|
763
|
|
|
764 function Contains (Container : Map; Key : Key_Type) return Boolean with
|
|
|
765 Global => null,
|
|
|
766 Post => Contains'Result = Contains (Model (Container), Key);
|
|
|
767 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
|
|
|
768
|
|
|
769 function Element (Container : Map; Key : Key_Type) return Element_Type with
|
|
|
770 Global => null,
|
|
|
771 Pre => Contains (Container, Key),
|
|
|
772 Post => Element'Result = Element (Model (Container), Key);
|
|
|
773 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
774
|
|
|
775 function Has_Element (Container : Map; Position : Cursor) return Boolean
|
|
|
776 with
|
|
|
777 Global => null,
|
|
|
778 Post =>
|
|
|
779 Has_Element'Result = P.Has_Key (Positions (Container), Position);
|
|
|
780 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
|
|
|
781
|
|
|
782 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
|
|
|
783 Global => null;
|
|
|
784
|
|
|
785 private
|
|
|
786 pragma SPARK_Mode (Off);
|
|
|
787
|
|
|
788 pragma Inline (Length);
|
|
|
789 pragma Inline (Is_Empty);
|
|
|
790 pragma Inline (Clear);
|
|
|
791 pragma Inline (Key);
|
|
|
792 pragma Inline (Element);
|
|
|
793 pragma Inline (Contains);
|
|
|
794 pragma Inline (Capacity);
|
|
|
795 pragma Inline (Has_Element);
|
|
|
796 pragma Inline (Equivalent_Keys);
|
|
|
797 pragma Inline (Next);
|
|
|
798
|
|
|
799 type Node_Type is record
|
|
|
800 Key : Key_Type;
|
|
|
801 Element : Element_Type;
|
|
|
802 Next : Count_Type;
|
|
|
803 Has_Element : Boolean := False;
|
|
|
804 end record;
|
|
|
805
|
|
|
806 package HT_Types is new
|
|
|
807 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
|
|
|
808
|
|
|
809 type Map (Capacity : Count_Type; Modulus : Hash_Type) is
|
|
|
810 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
|
|
|
811
|
|
|
812 Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
|
|
|
813
|
|
|
814 end Ada.Containers.Formal_Hashed_Maps;
|
