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-2018, 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 50with Ada.Containers.Functional_Vectors; 51with Ada.Containers.Functional_Maps; 52private with Ada.Containers.Hash_Tables; 53 54generic 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 63package Ada.Containers.Formal_Hashed_Maps with 64 SPARK_Mode 65is 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 784private 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 813end Ada.Containers.Formal_Hashed_Maps; 814