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 _ S E T S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2019, 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_Sets 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-- content of a container: Element, Next, Query_Element, Has_Element, Key, 42-- Iterate, Equivalent_Elements. This change is motivated by the need to 43-- have cursors which are valid on different containers (typically a 44-- container C and its previous version C'Old) for expressing properties, 45-- which is not possible if cursors encapsulate an access to the underlying 46-- container. 47 48with Ada.Containers.Functional_Maps; 49with Ada.Containers.Functional_Sets; 50with Ada.Containers.Functional_Vectors; 51private with Ada.Containers.Hash_Tables; 52 53generic 54 type Element_Type is private; 55 56 with function Hash (Element : Element_Type) return Hash_Type; 57 58 with function Equivalent_Elements 59 (Left : Element_Type; 60 Right : Element_Type) return Boolean is "="; 61 62package Ada.Containers.Formal_Hashed_Sets with 63 SPARK_Mode 64is 65 pragma Annotate (CodePeer, Skip_Analysis); 66 67 type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with 68 Iterable => (First => First, 69 Next => Next, 70 Has_Element => Has_Element, 71 Element => Element), 72 Default_Initial_Condition => Is_Empty (Set); 73 pragma Preelaborable_Initialization (Set); 74 75 type Cursor is record 76 Node : Count_Type; 77 end record; 78 79 No_Element : constant Cursor := (Node => 0); 80 81 function Length (Container : Set) return Count_Type with 82 Global => null, 83 Post => Length'Result <= Container.Capacity; 84 85 pragma Unevaluated_Use_Of_Old (Allow); 86 87 package Formal_Model with Ghost is 88 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; 89 90 package M is new Ada.Containers.Functional_Sets 91 (Element_Type => Element_Type, 92 Equivalent_Elements => Equivalent_Elements); 93 94 function "=" 95 (Left : M.Set; 96 Right : M.Set) return Boolean renames M."="; 97 98 function "<=" 99 (Left : M.Set; 100 Right : M.Set) return Boolean renames M."<="; 101 102 package E is new Ada.Containers.Functional_Vectors 103 (Element_Type => Element_Type, 104 Index_Type => Positive_Count_Type); 105 106 function "=" 107 (Left : E.Sequence; 108 Right : E.Sequence) return Boolean renames E."="; 109 110 function "<" 111 (Left : E.Sequence; 112 Right : E.Sequence) return Boolean renames E."<"; 113 114 function "<=" 115 (Left : E.Sequence; 116 Right : E.Sequence) return Boolean renames E."<="; 117 118 function Find 119 (Container : E.Sequence; 120 Item : Element_Type) return Count_Type 121 -- Search for Item in Container 122 123 with 124 Global => null, 125 Post => 126 (if Find'Result > 0 then 127 Find'Result <= E.Length (Container) 128 and Equivalent_Elements 129 (Item, E.Get (Container, Find'Result))); 130 131 function E_Elements_Included 132 (Left : E.Sequence; 133 Right : E.Sequence) return Boolean 134 -- The elements of Left are contained in Right 135 136 with 137 Global => null, 138 Post => 139 E_Elements_Included'Result = 140 (for all I in 1 .. E.Length (Left) => 141 Find (Right, E.Get (Left, I)) > 0 142 and then E.Get (Right, Find (Right, E.Get (Left, I))) = 143 E.Get (Left, I)); 144 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 145 146 function E_Elements_Included 147 (Left : E.Sequence; 148 Model : M.Set; 149 Right : E.Sequence) return Boolean 150 -- The elements of Container contained in Model are in Right 151 152 with 153 Global => null, 154 Post => 155 E_Elements_Included'Result = 156 (for all I in 1 .. E.Length (Left) => 157 (if M.Contains (Model, E.Get (Left, I)) then 158 Find (Right, E.Get (Left, I)) > 0 159 and then E.Get (Right, Find (Right, E.Get (Left, I))) = 160 E.Get (Left, I))); 161 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 162 163 function E_Elements_Included 164 (Container : E.Sequence; 165 Model : M.Set; 166 Left : E.Sequence; 167 Right : E.Sequence) return Boolean 168 -- The elements of Container contained in Model are in Left and others 169 -- are in Right. 170 171 with 172 Global => null, 173 Post => 174 E_Elements_Included'Result = 175 (for all I in 1 .. E.Length (Container) => 176 (if M.Contains (Model, E.Get (Container, I)) then 177 Find (Left, E.Get (Container, I)) > 0 178 and then E.Get (Left, Find (Left, E.Get (Container, I))) = 179 E.Get (Container, I) 180 else 181 Find (Right, E.Get (Container, I)) > 0 182 and then E.Get 183 (Right, Find (Right, E.Get (Container, I))) = 184 E.Get (Container, I))); 185 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 186 187 package P is new Ada.Containers.Functional_Maps 188 (Key_Type => Cursor, 189 Element_Type => Positive_Count_Type, 190 Equivalent_Keys => "=", 191 Enable_Handling_Of_Equivalence => False); 192 193 function "=" 194 (Left : P.Map; 195 Right : P.Map) return Boolean renames P."="; 196 197 function "<=" 198 (Left : P.Map; 199 Right : P.Map) return Boolean renames P."<="; 200 201 function Mapping_Preserved 202 (E_Left : E.Sequence; 203 E_Right : E.Sequence; 204 P_Left : P.Map; 205 P_Right : P.Map) return Boolean 206 with 207 Ghost, 208 Global => null, 209 Post => 210 (if Mapping_Preserved'Result then 211 212 -- Right contains all the cursors of Left 213 214 P.Keys_Included (P_Left, P_Right) 215 216 -- Right contains all the elements of Left 217 218 and E_Elements_Included (E_Left, E_Right) 219 220 -- Mappings from cursors to elements induced by E_Left, P_Left 221 -- and E_Right, P_Right are the same. 222 223 and (for all C of P_Left => 224 E.Get (E_Left, P.Get (P_Left, C)) = 225 E.Get (E_Right, P.Get (P_Right, C)))); 226 227 function Mapping_Preserved_Except 228 (E_Left : E.Sequence; 229 E_Right : E.Sequence; 230 P_Left : P.Map; 231 P_Right : P.Map; 232 Position : Cursor) return Boolean 233 with 234 Ghost, 235 Global => null, 236 Post => 237 (if Mapping_Preserved_Except'Result then 238 239 -- Right contains all the cursors of Left 240 241 P.Keys_Included (P_Left, P_Right) 242 243 -- Mappings from cursors to elements induced by E_Left, P_Left 244 -- and E_Right, P_Right are the same except for Position. 245 246 and (for all C of P_Left => 247 (if C /= Position then 248 E.Get (E_Left, P.Get (P_Left, C)) = 249 E.Get (E_Right, P.Get (P_Right, C))))); 250 251 function Model (Container : Set) return M.Set with 252 -- The high-level model of a set is a set of elements. Neither cursors 253 -- nor order of elements are represented in this model. Elements are 254 -- modeled up to equivalence. 255 256 Ghost, 257 Global => null, 258 Post => M.Length (Model'Result) = Length (Container); 259 260 function Elements (Container : Set) return E.Sequence with 261 -- The Elements sequence represents the underlying list structure of 262 -- sets that is used for iteration. It stores the actual values of 263 -- elements in the set. It does not model cursors. 264 265 Ghost, 266 Global => null, 267 Post => 268 E.Length (Elements'Result) = Length (Container) 269 270 -- It only contains keys contained in Model 271 272 and (for all Item of Elements'Result => 273 M.Contains (Model (Container), Item)) 274 275 -- It contains all the elements contained in Model 276 277 and (for all Item of Model (Container) => 278 (Find (Elements'Result, Item) > 0 279 and then Equivalent_Elements 280 (E.Get (Elements'Result, 281 Find (Elements'Result, Item)), 282 Item))) 283 284 -- It has no duplicate 285 286 and (for all I in 1 .. Length (Container) => 287 Find (Elements'Result, E.Get (Elements'Result, I)) = I) 288 289 and (for all I in 1 .. Length (Container) => 290 (for all J in 1 .. Length (Container) => 291 (if Equivalent_Elements 292 (E.Get (Elements'Result, I), 293 E.Get (Elements'Result, J)) 294 then I = J))); 295 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements); 296 297 function Positions (Container : Set) return P.Map with 298 -- The Positions map is used to model cursors. It only contains valid 299 -- cursors and maps them to their position in the container. 300 301 Ghost, 302 Global => null, 303 Post => 304 not P.Has_Key (Positions'Result, No_Element) 305 306 -- Positions of cursors are smaller than the container's length 307 308 and then 309 (for all I of Positions'Result => 310 P.Get (Positions'Result, I) in 1 .. Length (Container) 311 312 -- No two cursors have the same position. Note that we do not 313 -- state that there is a cursor in the map for each position, as 314 -- it is rarely needed. 315 316 and then 317 (for all J of Positions'Result => 318 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) 319 then I = J))); 320 321 procedure Lift_Abstraction_Level (Container : Set) with 322 -- Lift_Abstraction_Level is a ghost procedure that does nothing but 323 -- assume that we can access the same elements by iterating over 324 -- positions or cursors. 325 -- This information is not generally useful except when switching from 326 -- a low-level, cursor-aware view of a container, to a high-level, 327 -- position-based view. 328 329 Ghost, 330 Global => null, 331 Post => 332 (for all Item of Elements (Container) => 333 (for some I of Positions (Container) => 334 E.Get (Elements (Container), P.Get (Positions (Container), I)) = 335 Item)); 336 337 function Contains 338 (C : M.Set; 339 K : Element_Type) return Boolean renames M.Contains; 340 -- To improve readability of contracts, we rename the function used to 341 -- search for an element in the model to Contains. 342 343 end Formal_Model; 344 use Formal_Model; 345 346 Empty_Set : constant Set; 347 348 function "=" (Left, Right : Set) return Boolean with 349 Global => null, 350 Post => 351 "="'Result = 352 (Length (Left) = Length (Right) 353 and E_Elements_Included (Elements (Left), Elements (Right))) 354 and 355 "="'Result = 356 (E_Elements_Included (Elements (Left), Elements (Right)) 357 and E_Elements_Included (Elements (Right), Elements (Left))); 358 -- For each element in Left, set equality attempts to find the equal 359 -- element in Right; if a search fails, then set equality immediately 360 -- returns False. The search works by calling Hash to find the bucket in 361 -- the Right set that corresponds to the Left element. If the bucket is 362 -- non-empty, the search calls the generic formal element equality operator 363 -- to compare the element (in Left) to the element of each node in the 364 -- bucket (in Right); the search terminates when a matching node in the 365 -- bucket is found, or the nodes in the bucket are exhausted. (Note that 366 -- element equality is called here, not Equivalent_Elements. Set equality 367 -- is the only operation in which element equality is used. Compare set 368 -- equality to Equivalent_Sets, which does call Equivalent_Elements.) 369 370 function Equivalent_Sets (Left, Right : Set) return Boolean with 371 Global => null, 372 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right)); 373 -- Similar to set equality, with the difference that the element in Left is 374 -- compared to the elements in Right using the generic formal 375 -- Equivalent_Elements operation instead of element equality. 376 377 function To_Set (New_Item : Element_Type) return Set with 378 Global => null, 379 Post => 380 M.Is_Singleton (Model (To_Set'Result), New_Item) 381 and Length (To_Set'Result) = 1 382 and E.Get (Elements (To_Set'Result), 1) = New_Item; 383 -- Constructs a singleton set comprising New_Element. To_Set calls Hash to 384 -- determine the bucket for New_Item. 385 386 function Capacity (Container : Set) return Count_Type with 387 Global => null, 388 Post => Capacity'Result = Container.Capacity; 389 -- Returns the current capacity of the set. Capacity is the maximum length 390 -- before which rehashing in guaranteed not to occur. 391 392 procedure Reserve_Capacity 393 (Container : in out Set; 394 Capacity : Count_Type) 395 with 396 Global => null, 397 Pre => Capacity <= Container.Capacity, 398 Post => 399 Model (Container) = Model (Container)'Old 400 and Length (Container)'Old = Length (Container) 401 402 -- Actual elements are preserved 403 404 and E_Elements_Included 405 (Elements (Container), Elements (Container)'Old) 406 and E_Elements_Included 407 (Elements (Container)'Old, Elements (Container)); 408 -- If the value of the Capacity actual parameter is less or equal to 409 -- Container.Capacity, then the operation has no effect. Otherwise it 410 -- raises Capacity_Error (as no expansion of capacity is possible for a 411 -- bounded form). 412 413 function Is_Empty (Container : Set) return Boolean with 414 Global => null, 415 Post => Is_Empty'Result = (Length (Container) = 0); 416 -- Equivalent to Length (Container) = 0 417 418 procedure Clear (Container : in out Set) with 419 Global => null, 420 Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); 421 -- Removes all of the items from the set. This will deallocate all memory 422 -- associated with this set. 423 424 procedure Assign (Target : in out Set; Source : Set) with 425 Global => null, 426 Pre => Target.Capacity >= Length (Source), 427 Post => 428 Model (Target) = Model (Source) 429 and Length (Target) = Length (Source) 430 431 -- Actual elements are preserved 432 433 and E_Elements_Included (Elements (Target), Elements (Source)) 434 and E_Elements_Included (Elements (Source), Elements (Target)); 435 -- If Target denotes the same object as Source, then the operation has no 436 -- effect. If the Target capacity is less than the Source length, then 437 -- Assign raises Capacity_Error. Otherwise, Assign clears Target and then 438 -- copies the (active) elements from Source to Target. 439 440 function Copy 441 (Source : Set; 442 Capacity : Count_Type := 0) return Set 443 with 444 Global => null, 445 Pre => Capacity = 0 or else Capacity >= Source.Capacity, 446 Post => 447 Model (Copy'Result) = Model (Source) 448 and Elements (Copy'Result) = Elements (Source) 449 and Positions (Copy'Result) = Positions (Source) 450 and (if Capacity = 0 then 451 Copy'Result.Capacity = Source.Capacity 452 else 453 Copy'Result.Capacity = Capacity); 454 -- Constructs a new set object whose elements correspond to Source. If the 455 -- Capacity parameter is 0, then the capacity of the result is the same as 456 -- the length of Source. If the Capacity parameter is equal or greater than 457 -- the length of Source, then the capacity of the result is the specified 458 -- value. Otherwise, Copy raises Capacity_Error. If the Modulus parameter 459 -- is 0, then the modulus of the result is the value returned by a call to 460 -- Default_Modulus with the capacity parameter determined as above; 461 -- otherwise the modulus of the result is the specified value. 462 463 function Element 464 (Container : Set; 465 Position : Cursor) return Element_Type 466 with 467 Global => null, 468 Pre => Has_Element (Container, Position), 469 Post => 470 Element'Result = 471 E.Get (Elements (Container), P.Get (Positions (Container), Position)); 472 pragma Annotate (GNATprove, Inline_For_Proof, Element); 473 474 procedure Replace_Element 475 (Container : in out Set; 476 Position : Cursor; 477 New_Item : Element_Type) 478 with 479 Global => null, 480 Pre => Has_Element (Container, Position), 481 Post => 482 Length (Container) = Length (Container)'Old 483 484 -- Position now maps to New_Item 485 486 and Element (Container, Position) = New_Item 487 488 -- New_Item is contained in Container 489 490 and Contains (Model (Container), New_Item) 491 492 -- Other elements are preserved 493 494 and M.Included_Except 495 (Model (Container)'Old, 496 Model (Container), 497 Element (Container, Position)'Old) 498 and M.Included_Except 499 (Model (Container), 500 Model (Container)'Old, 501 New_Item) 502 503 -- Mapping from cursors to elements is preserved 504 505 and Mapping_Preserved_Except 506 (E_Left => Elements (Container)'Old, 507 E_Right => Elements (Container), 508 P_Left => Positions (Container)'Old, 509 P_Right => Positions (Container), 510 Position => Position) 511 and Positions (Container) = Positions (Container)'Old; 512 513 procedure Move (Target : in out Set; Source : in out Set) with 514 Global => null, 515 Pre => Target.Capacity >= Length (Source), 516 Post => 517 Length (Source) = 0 518 and Model (Target) = Model (Source)'Old 519 and Length (Target) = Length (Source)'Old 520 521 -- Actual elements are preserved 522 523 and E_Elements_Included (Elements (Target), Elements (Source)'Old) 524 and E_Elements_Included (Elements (Source)'Old, Elements (Target)); 525 -- Clears Target (if it's not empty), and then moves (not copies) the 526 -- buckets array and nodes from Source to Target. 527 528 procedure Insert 529 (Container : in out Set; 530 New_Item : Element_Type; 531 Position : out Cursor; 532 Inserted : out Boolean) 533 with 534 Global => null, 535 Pre => 536 Length (Container) < Container.Capacity 537 or Contains (Container, New_Item), 538 Post => 539 Contains (Container, New_Item) 540 and Has_Element (Container, Position) 541 and Equivalent_Elements (Element (Container, Position), New_Item), 542 Contract_Cases => 543 544 -- If New_Item is already in Container, it is not modified and Inserted 545 -- is set to False. 546 547 (Contains (Container, New_Item) => 548 not Inserted 549 and Model (Container) = Model (Container)'Old 550 and Elements (Container) = Elements (Container)'Old 551 and Positions (Container) = Positions (Container)'Old, 552 553 -- Otherwise, New_Item is inserted in Container and Inserted is set to 554 -- True. 555 556 others => 557 Inserted 558 and Length (Container) = Length (Container)'Old + 1 559 560 -- Position now maps to New_Item 561 562 and Element (Container, Position) = New_Item 563 564 -- Other elements are preserved 565 566 and Model (Container)'Old <= Model (Container) 567 and M.Included_Except 568 (Model (Container), 569 Model (Container)'Old, 570 New_Item) 571 572 -- Mapping from cursors to elements is preserved 573 574 and Mapping_Preserved 575 (E_Left => Elements (Container)'Old, 576 E_Right => Elements (Container), 577 P_Left => Positions (Container)'Old, 578 P_Right => Positions (Container)) 579 and P.Keys_Included_Except 580 (Positions (Container), 581 Positions (Container)'Old, 582 Position)); 583 -- Conditionally inserts New_Item into the set. If New_Item is already in 584 -- the set, then Inserted returns False and Position designates the node 585 -- containing the existing element (which is not modified). If New_Item is 586 -- not already in the set, then Inserted returns True and Position 587 -- designates the newly-inserted node containing New_Item. The search for 588 -- an existing element works as follows. Hash is called to determine 589 -- New_Item's bucket; if the bucket is non-empty, then Equivalent_Elements 590 -- is called to compare New_Item to the element of each node in that 591 -- bucket. If the bucket is empty, or there were no equivalent elements in 592 -- the bucket, the search "fails" and the New_Item is inserted in the set 593 -- (and Inserted returns True); otherwise, the search "succeeds" (and 594 -- Inserted returns False). 595 596 procedure Insert (Container : in out Set; New_Item : Element_Type) with 597 Global => null, 598 Pre => Length (Container) < Container.Capacity 599 and then (not Contains (Container, New_Item)), 600 Post => 601 Length (Container) = Length (Container)'Old + 1 602 and Contains (Container, New_Item) 603 and Element (Container, Find (Container, New_Item)) = New_Item 604 605 -- Other elements are preserved 606 607 and Model (Container)'Old <= Model (Container) 608 and M.Included_Except 609 (Model (Container), 610 Model (Container)'Old, 611 New_Item) 612 613 -- Mapping from cursors to elements is preserved 614 615 and Mapping_Preserved 616 (E_Left => Elements (Container)'Old, 617 E_Right => Elements (Container), 618 P_Left => Positions (Container)'Old, 619 P_Right => Positions (Container)) 620 and P.Keys_Included_Except 621 (Positions (Container), 622 Positions (Container)'Old, 623 Find (Container, New_Item)); 624 -- Attempts to insert New_Item into the set, performing the usual insertion 625 -- search (which involves calling both Hash and Equivalent_Elements); if 626 -- the search succeeds (New_Item is equivalent to an element already in the 627 -- set, and so was not inserted), then this operation raises 628 -- Constraint_Error. (This version of Insert is similar to Replace, but 629 -- having the opposite exception behavior. It is intended for use when you 630 -- want to assert that the item is not already in the set.) 631 632 procedure Include (Container : in out Set; New_Item : Element_Type) with 633 Global => null, 634 Pre => 635 Length (Container) < Container.Capacity 636 or Contains (Container, New_Item), 637 Post => 638 Contains (Container, New_Item) 639 and Element (Container, Find (Container, New_Item)) = New_Item, 640 Contract_Cases => 641 642 -- If an element equivalent to New_Item is already in Container, it is 643 -- replaced by New_Item. 644 645 (Contains (Container, New_Item) => 646 647 -- Elements are preserved modulo equivalence 648 649 Model (Container) = Model (Container)'Old 650 651 -- Cursors are preserved 652 653 and Positions (Container) = Positions (Container)'Old 654 655 -- The actual value of other elements is preserved 656 657 and E.Equal_Except 658 (Elements (Container)'Old, 659 Elements (Container), 660 P.Get (Positions (Container), Find (Container, New_Item))), 661 662 -- Otherwise, New_Item is inserted in Container 663 664 others => 665 Length (Container) = Length (Container)'Old + 1 666 667 -- Other elements are preserved 668 669 and Model (Container)'Old <= Model (Container) 670 and M.Included_Except 671 (Model (Container), 672 Model (Container)'Old, 673 New_Item) 674 675 -- Mapping from cursors to elements is preserved 676 677 and Mapping_Preserved 678 (E_Left => Elements (Container)'Old, 679 E_Right => Elements (Container), 680 P_Left => Positions (Container)'Old, 681 P_Right => Positions (Container)) 682 and P.Keys_Included_Except 683 (Positions (Container), 684 Positions (Container)'Old, 685 Find (Container, New_Item))); 686 -- Attempts to insert New_Item into the set. If an element equivalent to 687 -- New_Item is already in the set (the insertion search succeeded, and 688 -- hence New_Item was not inserted), then the value of New_Item is assigned 689 -- to the existing element. (This insertion operation only raises an 690 -- exception if cursor tampering occurs. It is intended for use when you 691 -- want to insert the item in the set, and you don't care whether an 692 -- equivalent element is already present.) 693 694 procedure Replace (Container : in out Set; New_Item : Element_Type) with 695 Global => null, 696 Pre => Contains (Container, New_Item), 697 Post => 698 699 -- Elements are preserved modulo equivalence 700 701 Model (Container) = Model (Container)'Old 702 and Contains (Container, New_Item) 703 704 -- Cursors are preserved 705 706 and Positions (Container) = Positions (Container)'Old 707 708 -- The element equivalent to New_Item in Container is replaced by 709 -- New_Item. 710 711 and Element (Container, Find (Container, New_Item)) = New_Item 712 and E.Equal_Except 713 (Elements (Container)'Old, 714 Elements (Container), 715 P.Get (Positions (Container), Find (Container, New_Item))); 716 -- Searches for New_Item in the set; if the search fails (because an 717 -- equivalent element was not in the set), then it raises 718 -- Constraint_Error. Otherwise, the existing element is assigned the value 719 -- New_Item. (This is similar to Insert, but with the opposite exception 720 -- behavior. It is intended for use when you want to assert that the item 721 -- is already in the set.) 722 723 procedure Exclude (Container : in out Set; Item : Element_Type) with 724 Global => null, 725 Post => not Contains (Container, Item), 726 Contract_Cases => 727 728 -- If Item is not in Container, nothing is changed 729 730 (not Contains (Container, Item) => 731 Model (Container) = Model (Container)'Old 732 and Elements (Container) = Elements (Container)'Old 733 and Positions (Container) = Positions (Container)'Old, 734 735 -- Otherwise, Item is removed from Container 736 737 others => 738 Length (Container) = Length (Container)'Old - 1 739 740 -- Other elements are preserved 741 742 and Model (Container) <= Model (Container)'Old 743 and M.Included_Except 744 (Model (Container)'Old, 745 Model (Container), 746 Item) 747 748 -- Mapping from cursors to elements is preserved 749 750 and Mapping_Preserved 751 (E_Left => Elements (Container), 752 E_Right => Elements (Container)'Old, 753 P_Left => Positions (Container), 754 P_Right => Positions (Container)'Old) 755 and P.Keys_Included_Except 756 (Positions (Container)'Old, 757 Positions (Container), 758 Find (Container, Item)'Old)); 759 -- Searches for Item in the set, and if found, removes its node from the 760 -- set and then deallocates it. The search works as follows. The operation 761 -- calls Hash to determine the item's bucket; if the bucket is not empty, 762 -- it calls Equivalent_Elements to compare Item to the element of each node 763 -- in the bucket. (This is the deletion analog of Include. It is intended 764 -- for use when you want to remove the item from the set, but don't care 765 -- whether the item is already in the set.) 766 767 procedure Delete (Container : in out Set; Item : Element_Type) with 768 Global => null, 769 Pre => Contains (Container, Item), 770 Post => 771 Length (Container) = Length (Container)'Old - 1 772 773 -- Item is no longer in Container 774 775 and not Contains (Container, Item) 776 777 -- Other elements are preserved 778 779 and Model (Container) <= Model (Container)'Old 780 and M.Included_Except 781 (Model (Container)'Old, 782 Model (Container), 783 Item) 784 785 -- Mapping from cursors to elements is preserved 786 787 and Mapping_Preserved 788 (E_Left => Elements (Container), 789 E_Right => Elements (Container)'Old, 790 P_Left => Positions (Container), 791 P_Right => Positions (Container)'Old) 792 and P.Keys_Included_Except 793 (Positions (Container)'Old, 794 Positions (Container), 795 Find (Container, Item)'Old); 796 -- Searches for Item in the set (which involves calling both Hash and 797 -- Equivalent_Elements). If the search fails, then the operation raises 798 -- Constraint_Error. Otherwise it removes the node from the set and then 799 -- deallocates it. (This is the deletion analog of non-conditional 800 -- Insert. It is intended for use when you want to assert that the item is 801 -- already in the set.) 802 803 procedure Delete (Container : in out Set; Position : in out Cursor) with 804 Global => null, 805 Pre => Has_Element (Container, Position), 806 Post => 807 Position = No_Element 808 and Length (Container) = Length (Container)'Old - 1 809 810 -- The element at position Position is no longer in Container 811 812 and not Contains (Container, Element (Container, Position)'Old) 813 and not P.Has_Key (Positions (Container), Position'Old) 814 815 -- Other elements are preserved 816 817 and Model (Container) <= Model (Container)'Old 818 and M.Included_Except 819 (Model (Container)'Old, 820 Model (Container), 821 Element (Container, Position)'Old) 822 823 -- Mapping from cursors to elements is preserved 824 825 and Mapping_Preserved 826 (E_Left => Elements (Container), 827 E_Right => Elements (Container)'Old, 828 P_Left => Positions (Container), 829 P_Right => Positions (Container)'Old) 830 and P.Keys_Included_Except 831 (Positions (Container)'Old, 832 Positions (Container), 833 Position'Old); 834 -- Removes the node designated by Position from the set, and then 835 -- deallocates the node. The operation calls Hash to determine the bucket, 836 -- and then compares Position to each node in the bucket until there's a 837 -- match (it does not call Equivalent_Elements). 838 839 procedure Union (Target : in out Set; Source : Set) with 840 Global => null, 841 Pre => 842 Length (Source) - Length (Target and Source) <= 843 Target.Capacity - Length (Target), 844 Post => 845 Length (Target) = Length (Target)'Old 846 - M.Num_Overlaps (Model (Target)'Old, Model (Source)) 847 + Length (Source) 848 849 -- Elements already in Target are still in Target 850 851 and Model (Target)'Old <= Model (Target) 852 853 -- Elements of Source are included in Target 854 855 and Model (Source) <= Model (Target) 856 857 -- Elements of Target come from either Source or Target 858 859 and M.Included_In_Union 860 (Model (Target), Model (Source), Model (Target)'Old) 861 862 -- Actual value of elements come from either Left or Right 863 864 and E_Elements_Included 865 (Elements (Target), 866 Model (Target)'Old, 867 Elements (Target)'Old, 868 Elements (Source)) 869 870 and E_Elements_Included 871 (Elements (Target)'Old, Model (Target)'Old, Elements (Target)) 872 873 and E_Elements_Included 874 (Elements (Source), 875 Model (Target)'Old, 876 Elements (Source), 877 Elements (Target)) 878 879 -- Mapping from cursors of Target to elements is preserved 880 881 and Mapping_Preserved 882 (E_Left => Elements (Target)'Old, 883 E_Right => Elements (Target), 884 P_Left => Positions (Target)'Old, 885 P_Right => Positions (Target)); 886 -- Iterates over the Source set, and conditionally inserts each element 887 -- into Target. 888 889 function Union (Left, Right : Set) return Set with 890 Global => null, 891 Pre => Length (Left) <= Count_Type'Last - Length (Right), 892 Post => 893 Length (Union'Result) = Length (Left) 894 - M.Num_Overlaps (Model (Left), Model (Right)) 895 + Length (Right) 896 897 -- Elements of Left and Right are in the result of Union 898 899 and Model (Left) <= Model (Union'Result) 900 and Model (Right) <= Model (Union'Result) 901 902 -- Elements of the result of union come from either Left or Right 903 904 and 905 M.Included_In_Union 906 (Model (Union'Result), Model (Left), Model (Right)) 907 908 -- Actual value of elements come from either Left or Right 909 910 and E_Elements_Included 911 (Elements (Union'Result), 912 Model (Left), 913 Elements (Left), 914 Elements (Right)) 915 916 and E_Elements_Included 917 (Elements (Left), Model (Left), Elements (Union'Result)) 918 919 and E_Elements_Included 920 (Elements (Right), 921 Model (Left), 922 Elements (Right), 923 Elements (Union'Result)); 924 -- The operation first copies the Left set to the result, and then iterates 925 -- over the Right set to conditionally insert each element into the result. 926 927 function "or" (Left, Right : Set) return Set renames Union; 928 929 procedure Intersection (Target : in out Set; Source : Set) with 930 Global => null, 931 Post => 932 Length (Target) = 933 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 934 935 -- Elements of Target were already in Target 936 937 and Model (Target) <= Model (Target)'Old 938 939 -- Elements of Target are in Source 940 941 and Model (Target) <= Model (Source) 942 943 -- Elements both in Source and Target are in the intersection 944 945 and M.Includes_Intersection 946 (Model (Target), Model (Source), Model (Target)'Old) 947 948 -- Actual value of elements of Target is preserved 949 950 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 951 and E_Elements_Included 952 (Elements (Target)'Old, Model (Source), Elements (Target)) 953 954 -- Mapping from cursors of Target to elements is preserved 955 956 and Mapping_Preserved 957 (E_Left => Elements (Target), 958 E_Right => Elements (Target)'Old, 959 P_Left => Positions (Target), 960 P_Right => Positions (Target)'Old); 961 -- Iterates over the Target set (calling First and Next), calling Find to 962 -- determine whether the element is in Source. If an equivalent element is 963 -- not found in Source, the element is deleted from Target. 964 965 function Intersection (Left, Right : Set) return Set with 966 Global => null, 967 Post => 968 Length (Intersection'Result) = 969 M.Num_Overlaps (Model (Left), Model (Right)) 970 971 -- Elements in the result of Intersection are in Left and Right 972 973 and Model (Intersection'Result) <= Model (Left) 974 and Model (Intersection'Result) <= Model (Right) 975 976 -- Elements both in Left and Right are in the result of Intersection 977 978 and M.Includes_Intersection 979 (Model (Intersection'Result), Model (Left), Model (Right)) 980 981 -- Actual value of elements come from Left 982 983 and E_Elements_Included 984 (Elements (Intersection'Result), Elements (Left)) 985 986 and E_Elements_Included 987 (Elements (Left), Model (Right), 988 Elements (Intersection'Result)); 989 -- Iterates over the Left set, calling Find to determine whether the 990 -- element is in Right. If an equivalent element is found, it is inserted 991 -- into the result set. 992 993 function "and" (Left, Right : Set) return Set renames Intersection; 994 995 procedure Difference (Target : in out Set; Source : Set) with 996 Global => null, 997 Post => 998 Length (Target) = Length (Target)'Old - 999 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 1000 1001 -- Elements of Target were already in Target 1002 1003 and Model (Target) <= Model (Target)'Old 1004 1005 -- Elements of Target are not in Source 1006 1007 and M.No_Overlap (Model (Target), Model (Source)) 1008 1009 -- Elements in Target but not in Source are in the difference 1010 1011 and M.Included_In_Union 1012 (Model (Target)'Old, Model (Target), Model (Source)) 1013 1014 -- Actual value of elements of Target is preserved 1015 1016 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 1017 and E_Elements_Included 1018 (Elements (Target)'Old, Model (Target), Elements (Target)) 1019 1020 -- Mapping from cursors of Target to elements is preserved 1021 1022 and Mapping_Preserved 1023 (E_Left => Elements (Target), 1024 E_Right => Elements (Target)'Old, 1025 P_Left => Positions (Target), 1026 P_Right => Positions (Target)'Old); 1027 -- Iterates over the Source (calling First and Next), calling Find to 1028 -- determine whether the element is in Target. If an equivalent element is 1029 -- found, it is deleted from Target. 1030 1031 function Difference (Left, Right : Set) return Set with 1032 Global => null, 1033 Post => 1034 Length (Difference'Result) = Length (Left) - 1035 M.Num_Overlaps (Model (Left), Model (Right)) 1036 1037 -- Elements of the result of Difference are in Left 1038 1039 and Model (Difference'Result) <= Model (Left) 1040 1041 -- Elements of the result of Difference are in Right 1042 1043 and M.No_Overlap (Model (Difference'Result), Model (Right)) 1044 1045 -- Elements in Left but not in Right are in the difference 1046 1047 and M.Included_In_Union 1048 (Model (Left), Model (Difference'Result), Model (Right)) 1049 1050 -- Actual value of elements come from Left 1051 1052 and E_Elements_Included 1053 (Elements (Difference'Result), Elements (Left)) 1054 1055 and E_Elements_Included 1056 (Elements (Left), 1057 Model (Difference'Result), 1058 Elements (Difference'Result)); 1059 -- Iterates over the Left set, calling Find to determine whether the 1060 -- element is in the Right set. If an equivalent element is not found, the 1061 -- element is inserted into the result set. 1062 1063 function "-" (Left, Right : Set) return Set renames Difference; 1064 1065 procedure Symmetric_Difference (Target : in out Set; Source : Set) with 1066 Global => null, 1067 Pre => 1068 Length (Source) - Length (Target and Source) <= 1069 Target.Capacity - Length (Target) + Length (Target and Source), 1070 Post => 1071 Length (Target) = Length (Target)'Old - 1072 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + 1073 Length (Source) 1074 1075 -- Elements of the difference were not both in Source and in Target 1076 1077 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source)) 1078 1079 -- Elements in Target but not in Source are in the difference 1080 1081 and M.Included_In_Union 1082 (Model (Target)'Old, Model (Target), Model (Source)) 1083 1084 -- Elements in Source but not in Target are in the difference 1085 1086 and M.Included_In_Union 1087 (Model (Source), Model (Target), Model (Target)'Old) 1088 1089 -- Actual value of elements come from either Left or Right 1090 1091 and E_Elements_Included 1092 (Elements (Target), 1093 Model (Target)'Old, 1094 Elements (Target)'Old, 1095 Elements (Source)) 1096 1097 and E_Elements_Included 1098 (Elements (Target)'Old, Model (Target), Elements (Target)) 1099 1100 and E_Elements_Included 1101 (Elements (Source), Model (Target), Elements (Target)); 1102 -- The operation iterates over the Source set, searching for the element 1103 -- in Target (calling Hash and Equivalent_Elements). If an equivalent 1104 -- element is found, it is removed from Target; otherwise it is inserted 1105 -- into Target. 1106 1107 function Symmetric_Difference (Left, Right : Set) return Set with 1108 Global => null, 1109 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1110 Post => 1111 Length (Symmetric_Difference'Result) = Length (Left) - 1112 2 * M.Num_Overlaps (Model (Left), Model (Right)) + 1113 Length (Right) 1114 1115 -- Elements of the difference were not both in Left and Right 1116 1117 and M.Not_In_Both 1118 (Model (Symmetric_Difference'Result), 1119 Model (Left), 1120 Model (Right)) 1121 1122 -- Elements in Left but not in Right are in the difference 1123 1124 and M.Included_In_Union 1125 (Model (Left), 1126 Model (Symmetric_Difference'Result), 1127 Model (Right)) 1128 1129 -- Elements in Right but not in Left are in the difference 1130 1131 and M.Included_In_Union 1132 (Model (Right), 1133 Model (Symmetric_Difference'Result), 1134 Model (Left)) 1135 1136 -- Actual value of elements come from either Left or Right 1137 1138 and E_Elements_Included 1139 (Elements (Symmetric_Difference'Result), 1140 Model (Left), 1141 Elements (Left), 1142 Elements (Right)) 1143 1144 and E_Elements_Included 1145 (Elements (Left), 1146 Model (Symmetric_Difference'Result), 1147 Elements (Symmetric_Difference'Result)) 1148 1149 and E_Elements_Included 1150 (Elements (Right), 1151 Model (Symmetric_Difference'Result), 1152 Elements (Symmetric_Difference'Result)); 1153 -- The operation first iterates over the Left set. It calls Find to 1154 -- determine whether the element is in the Right set. If no equivalent 1155 -- element is found, the element from Left is inserted into the result. The 1156 -- operation then iterates over the Right set, to determine whether the 1157 -- element is in the Left set. If no equivalent element is found, the Right 1158 -- element is inserted into the result. 1159 1160 function "xor" (Left, Right : Set) return Set 1161 renames Symmetric_Difference; 1162 1163 function Overlap (Left, Right : Set) return Boolean with 1164 Global => null, 1165 Post => 1166 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); 1167 -- Iterates over the Left set (calling First and Next), calling Find to 1168 -- determine whether the element is in the Right set. If an equivalent 1169 -- element is found, the operation immediately returns True. The operation 1170 -- returns False if the iteration over Left terminates without finding any 1171 -- equivalent element in Right. 1172 1173 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with 1174 Global => null, 1175 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); 1176 -- Iterates over Subset (calling First and Next), calling Find to determine 1177 -- whether the element is in Of_Set. If no equivalent element is found in 1178 -- Of_Set, the operation immediately returns False. The operation returns 1179 -- True if the iteration over Subset terminates without finding an element 1180 -- not in Of_Set (that is, every element in Subset is equivalent to an 1181 -- element in Of_Set). 1182 1183 function First (Container : Set) return Cursor with 1184 Global => null, 1185 Contract_Cases => 1186 (Length (Container) = 0 => 1187 First'Result = No_Element, 1188 1189 others => 1190 Has_Element (Container, First'Result) 1191 and P.Get (Positions (Container), First'Result) = 1); 1192 -- Returns a cursor that designates the first non-empty bucket, by 1193 -- searching from the beginning of the buckets array. 1194 1195 function Next (Container : Set; Position : Cursor) return Cursor with 1196 Global => null, 1197 Pre => 1198 Has_Element (Container, Position) or else Position = No_Element, 1199 Contract_Cases => 1200 (Position = No_Element 1201 or else P.Get (Positions (Container), Position) = Length (Container) 1202 => 1203 Next'Result = No_Element, 1204 1205 others => 1206 Has_Element (Container, Next'Result) 1207 and then P.Get (Positions (Container), Next'Result) = 1208 P.Get (Positions (Container), Position) + 1); 1209 -- Returns a cursor that designates the node that follows the current one 1210 -- designated by Position. If Position designates the last node in its 1211 -- bucket, the operation calls Hash to compute the index of this bucket, 1212 -- and searches the buckets array for the first non-empty bucket, starting 1213 -- from that index; otherwise, it simply follows the link to the next node 1214 -- in the same bucket. 1215 1216 procedure Next (Container : Set; Position : in out Cursor) with 1217 Global => null, 1218 Pre => 1219 Has_Element (Container, Position) or else Position = No_Element, 1220 Contract_Cases => 1221 (Position = No_Element 1222 or else P.Get (Positions (Container), Position) = Length (Container) 1223 => 1224 Position = No_Element, 1225 1226 others => 1227 Has_Element (Container, Position) 1228 and then P.Get (Positions (Container), Position) = 1229 P.Get (Positions (Container), Position'Old) + 1); 1230 -- Equivalent to Position := Next (Position) 1231 1232 function Find 1233 (Container : Set; 1234 Item : Element_Type) return Cursor 1235 with 1236 Global => null, 1237 Contract_Cases => 1238 1239 -- If Item is not contained in Container, Find returns No_Element 1240 1241 (not Contains (Model (Container), Item) => 1242 Find'Result = No_Element, 1243 1244 -- Otherwise, Find returns a valid cursor in Container 1245 1246 others => 1247 P.Has_Key (Positions (Container), Find'Result) 1248 and P.Get (Positions (Container), Find'Result) = 1249 Find (Elements (Container), Item) 1250 1251 -- The element designated by the result of Find is Item 1252 1253 and Equivalent_Elements 1254 (Element (Container, Find'Result), Item)); 1255 -- Searches for Item in the set. Find calls Hash to determine the item's 1256 -- bucket; if the bucket is not empty, it calls Equivalent_Elements to 1257 -- compare Item to each element in the bucket. If the search succeeds, Find 1258 -- returns a cursor designating the node containing the equivalent element; 1259 -- otherwise, it returns No_Element. 1260 1261 function Contains (Container : Set; Item : Element_Type) return Boolean with 1262 Global => null, 1263 Post => Contains'Result = Contains (Model (Container), Item); 1264 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 1265 1266 function Has_Element (Container : Set; Position : Cursor) return Boolean 1267 with 1268 Global => null, 1269 Post => 1270 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1271 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1272 1273 function Default_Modulus (Capacity : Count_Type) return Hash_Type with 1274 Global => null; 1275 1276 generic 1277 type Key_Type (<>) is private; 1278 1279 with function Key (Element : Element_Type) return Key_Type; 1280 1281 with function Hash (Key : Key_Type) return Hash_Type; 1282 1283 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; 1284 1285 package Generic_Keys with SPARK_Mode is 1286 1287 package Formal_Model with Ghost is 1288 1289 function M_Included_Except 1290 (Left : M.Set; 1291 Right : M.Set; 1292 Key : Key_Type) return Boolean 1293 with 1294 Global => null, 1295 Post => 1296 M_Included_Except'Result = 1297 (for all E of Left => 1298 Contains (Right, E) 1299 or Equivalent_Keys (Generic_Keys.Key (E), Key)); 1300 1301 end Formal_Model; 1302 use Formal_Model; 1303 1304 function Key (Container : Set; Position : Cursor) return Key_Type with 1305 Global => null, 1306 Post => Key'Result = Key (Element (Container, Position)); 1307 pragma Annotate (GNATprove, Inline_For_Proof, Key); 1308 1309 function Element (Container : Set; Key : Key_Type) return Element_Type 1310 with 1311 Global => null, 1312 Pre => Contains (Container, Key), 1313 Post => 1314 Element'Result = Element (Container, Find (Container, Key)); 1315 pragma Annotate (GNATprove, Inline_For_Proof, Element); 1316 1317 procedure Replace 1318 (Container : in out Set; 1319 Key : Key_Type; 1320 New_Item : Element_Type) 1321 with 1322 Global => null, 1323 Pre => Contains (Container, Key), 1324 Post => 1325 Length (Container) = Length (Container)'Old 1326 1327 -- Key now maps to New_Item 1328 1329 and Element (Container, Key) = New_Item 1330 1331 -- New_Item is contained in Container 1332 1333 and Contains (Model (Container), New_Item) 1334 1335 -- Other elements are preserved 1336 1337 and M_Included_Except 1338 (Model (Container)'Old, 1339 Model (Container), 1340 Key) 1341 and M.Included_Except 1342 (Model (Container), 1343 Model (Container)'Old, 1344 New_Item) 1345 1346 -- Mapping from cursors to elements is preserved 1347 1348 and Mapping_Preserved_Except 1349 (E_Left => Elements (Container)'Old, 1350 E_Right => Elements (Container), 1351 P_Left => Positions (Container)'Old, 1352 P_Right => Positions (Container), 1353 Position => Find (Container, Key)) 1354 and Positions (Container) = Positions (Container)'Old; 1355 1356 procedure Exclude (Container : in out Set; Key : Key_Type) with 1357 Global => null, 1358 Post => not Contains (Container, Key), 1359 Contract_Cases => 1360 1361 -- If Key is not in Container, nothing is changed 1362 1363 (not Contains (Container, Key) => 1364 Model (Container) = Model (Container)'Old 1365 and Elements (Container) = Elements (Container)'Old 1366 and Positions (Container) = Positions (Container)'Old, 1367 1368 -- Otherwise, Key is removed from Container 1369 1370 others => 1371 Length (Container) = Length (Container)'Old - 1 1372 1373 -- Other elements are preserved 1374 1375 and Model (Container) <= Model (Container)'Old 1376 and M_Included_Except 1377 (Model (Container)'Old, 1378 Model (Container), 1379 Key) 1380 1381 -- Mapping from cursors to elements is preserved 1382 1383 and Mapping_Preserved 1384 (E_Left => Elements (Container), 1385 E_Right => Elements (Container)'Old, 1386 P_Left => Positions (Container), 1387 P_Right => Positions (Container)'Old) 1388 and P.Keys_Included_Except 1389 (Positions (Container)'Old, 1390 Positions (Container), 1391 Find (Container, Key)'Old)); 1392 1393 procedure Delete (Container : in out Set; Key : Key_Type) with 1394 Global => null, 1395 Pre => Contains (Container, Key), 1396 Post => 1397 Length (Container) = Length (Container)'Old - 1 1398 1399 -- Key is no longer in Container 1400 1401 and not Contains (Container, Key) 1402 1403 -- Other elements are preserved 1404 1405 and Model (Container) <= Model (Container)'Old 1406 and M_Included_Except 1407 (Model (Container)'Old, 1408 Model (Container), 1409 Key) 1410 1411 -- Mapping from cursors to elements is preserved 1412 1413 and Mapping_Preserved 1414 (E_Left => Elements (Container), 1415 E_Right => Elements (Container)'Old, 1416 P_Left => Positions (Container), 1417 P_Right => Positions (Container)'Old) 1418 and P.Keys_Included_Except 1419 (Positions (Container)'Old, 1420 Positions (Container), 1421 Find (Container, Key)'Old); 1422 1423 function Find (Container : Set; Key : Key_Type) return Cursor with 1424 Global => null, 1425 Contract_Cases => 1426 1427 -- If Key is not contained in Container, Find returns No_Element 1428 1429 ((for all E of Model (Container) => 1430 not Equivalent_Keys (Key, Generic_Keys.Key (E))) => 1431 Find'Result = No_Element, 1432 1433 -- Otherwise, Find returns a valid cursor in Container 1434 1435 others => 1436 P.Has_Key (Positions (Container), Find'Result) 1437 1438 -- The key designated by the result of Find is Key 1439 1440 and Equivalent_Keys 1441 (Generic_Keys.Key (Container, Find'Result), Key)); 1442 1443 function Contains (Container : Set; Key : Key_Type) return Boolean with 1444 Global => null, 1445 Post => 1446 Contains'Result = 1447 (for some E of Model (Container) => 1448 Equivalent_Keys (Key, Generic_Keys.Key (E))); 1449 1450 end Generic_Keys; 1451 1452private 1453 pragma SPARK_Mode (Off); 1454 1455 pragma Inline (Next); 1456 1457 type Node_Type is 1458 record 1459 Element : Element_Type; 1460 Next : Count_Type; 1461 Has_Element : Boolean := False; 1462 end record; 1463 1464 package HT_Types is new 1465 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); 1466 1467 type Set (Capacity : Count_Type; Modulus : Hash_Type) is 1468 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; 1469 1470 use HT_Types; 1471 1472 Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>); 1473 1474end Ada.Containers.Formal_Hashed_Sets; 1475