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