Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cfhama.ads @ 111:04ced10e8804

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
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;