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-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_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 359 function Equivalent_Sets (Left, Right : Set) return Boolean with 360 Global => null, 361 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right)); 362 363 function To_Set (New_Item : Element_Type) return Set with 364 Global => null, 365 Post => 366 M.Is_Singleton (Model (To_Set'Result), New_Item) 367 and Length (To_Set'Result) = 1 368 and E.Get (Elements (To_Set'Result), 1) = New_Item; 369 370 function Capacity (Container : Set) return Count_Type with 371 Global => null, 372 Post => Capacity'Result = Container.Capacity; 373 374 procedure Reserve_Capacity 375 (Container : in out Set; 376 Capacity : Count_Type) 377 with 378 Global => null, 379 Pre => Capacity <= Container.Capacity, 380 Post => 381 Model (Container) = Model (Container)'Old 382 and Length (Container)'Old = Length (Container) 383 384 -- Actual elements are preserved 385 386 and E_Elements_Included 387 (Elements (Container), Elements (Container)'Old) 388 and E_Elements_Included 389 (Elements (Container)'Old, Elements (Container)); 390 391 function Is_Empty (Container : Set) return Boolean with 392 Global => null, 393 Post => Is_Empty'Result = (Length (Container) = 0); 394 395 procedure Clear (Container : in out Set) with 396 Global => null, 397 Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); 398 399 procedure Assign (Target : in out Set; Source : Set) with 400 Global => null, 401 Pre => Target.Capacity >= Length (Source), 402 Post => 403 Model (Target) = Model (Source) 404 and Length (Target) = Length (Source) 405 406 -- Actual elements are preserved 407 408 and E_Elements_Included (Elements (Target), Elements (Source)) 409 and E_Elements_Included (Elements (Source), Elements (Target)); 410 411 function Copy 412 (Source : Set; 413 Capacity : Count_Type := 0) return Set 414 with 415 Global => null, 416 Pre => Capacity = 0 or else Capacity >= Source.Capacity, 417 Post => 418 Model (Copy'Result) = Model (Source) 419 and Elements (Copy'Result) = Elements (Source) 420 and Positions (Copy'Result) = Positions (Source) 421 and (if Capacity = 0 then 422 Copy'Result.Capacity = Source.Capacity 423 else 424 Copy'Result.Capacity = Capacity); 425 426 function Element 427 (Container : Set; 428 Position : Cursor) return Element_Type 429 with 430 Global => null, 431 Pre => Has_Element (Container, Position), 432 Post => 433 Element'Result = 434 E.Get (Elements (Container), P.Get (Positions (Container), Position)); 435 pragma Annotate (GNATprove, Inline_For_Proof, Element); 436 437 procedure Replace_Element 438 (Container : in out Set; 439 Position : Cursor; 440 New_Item : Element_Type) 441 with 442 Global => null, 443 Pre => Has_Element (Container, Position), 444 Post => 445 Length (Container) = Length (Container)'Old 446 447 -- Position now maps to New_Item 448 449 and Element (Container, Position) = New_Item 450 451 -- New_Item is contained in Container 452 453 and Contains (Model (Container), New_Item) 454 455 -- Other elements are preserved 456 457 and M.Included_Except 458 (Model (Container)'Old, 459 Model (Container), 460 Element (Container, Position)'Old) 461 and M.Included_Except 462 (Model (Container), 463 Model (Container)'Old, 464 New_Item) 465 466 -- Mapping from cursors to elements is preserved 467 468 and Mapping_Preserved_Except 469 (E_Left => Elements (Container)'Old, 470 E_Right => Elements (Container), 471 P_Left => Positions (Container)'Old, 472 P_Right => Positions (Container), 473 Position => Position) 474 and Positions (Container) = Positions (Container)'Old; 475 476 procedure Move (Target : in out Set; Source : in out Set) with 477 Global => null, 478 Pre => Target.Capacity >= Length (Source), 479 Post => 480 Length (Source) = 0 481 and Model (Target) = Model (Source)'Old 482 and Length (Target) = Length (Source)'Old 483 484 -- Actual elements are preserved 485 486 and E_Elements_Included (Elements (Target), Elements (Source)'Old) 487 and E_Elements_Included (Elements (Source)'Old, Elements (Target)); 488 489 procedure Insert 490 (Container : in out Set; 491 New_Item : Element_Type; 492 Position : out Cursor; 493 Inserted : out Boolean) 494 with 495 Global => null, 496 Pre => 497 Length (Container) < Container.Capacity 498 or Contains (Container, New_Item), 499 Post => 500 Contains (Container, New_Item) 501 and Has_Element (Container, Position) 502 and Equivalent_Elements (Element (Container, Position), New_Item), 503 Contract_Cases => 504 505 -- If New_Item is already in Container, it is not modified and Inserted 506 -- is set to False. 507 508 (Contains (Container, New_Item) => 509 not Inserted 510 and Model (Container) = Model (Container)'Old 511 and Elements (Container) = Elements (Container)'Old 512 and Positions (Container) = Positions (Container)'Old, 513 514 -- Otherwise, New_Item is inserted in Container and Inserted is set to 515 -- True. 516 517 others => 518 Inserted 519 and Length (Container) = Length (Container)'Old + 1 520 521 -- Position now maps to New_Item 522 523 and Element (Container, Position) = New_Item 524 525 -- Other elements are preserved 526 527 and Model (Container)'Old <= Model (Container) 528 and M.Included_Except 529 (Model (Container), 530 Model (Container)'Old, 531 New_Item) 532 533 -- Mapping from cursors to elements is preserved 534 535 and Mapping_Preserved 536 (E_Left => Elements (Container)'Old, 537 E_Right => Elements (Container), 538 P_Left => Positions (Container)'Old, 539 P_Right => Positions (Container)) 540 and P.Keys_Included_Except 541 (Positions (Container), 542 Positions (Container)'Old, 543 Position)); 544 545 procedure Insert (Container : in out Set; New_Item : Element_Type) with 546 Global => null, 547 Pre => Length (Container) < Container.Capacity 548 and then (not Contains (Container, New_Item)), 549 Post => 550 Length (Container) = Length (Container)'Old + 1 551 and Contains (Container, New_Item) 552 and Element (Container, Find (Container, New_Item)) = New_Item 553 554 -- Other elements are preserved 555 556 and Model (Container)'Old <= Model (Container) 557 and M.Included_Except 558 (Model (Container), 559 Model (Container)'Old, 560 New_Item) 561 562 -- Mapping from cursors to elements is preserved 563 564 and Mapping_Preserved 565 (E_Left => Elements (Container)'Old, 566 E_Right => Elements (Container), 567 P_Left => Positions (Container)'Old, 568 P_Right => Positions (Container)) 569 and P.Keys_Included_Except 570 (Positions (Container), 571 Positions (Container)'Old, 572 Find (Container, New_Item)); 573 574 procedure Include (Container : in out Set; New_Item : Element_Type) with 575 Global => null, 576 Pre => 577 Length (Container) < Container.Capacity 578 or Contains (Container, New_Item), 579 Post => 580 Contains (Container, New_Item) 581 and Element (Container, Find (Container, New_Item)) = New_Item, 582 Contract_Cases => 583 584 -- If an element equivalent to New_Item is already in Container, it is 585 -- replaced by New_Item. 586 587 (Contains (Container, New_Item) => 588 589 -- Elements are preserved modulo equivalence 590 591 Model (Container) = Model (Container)'Old 592 593 -- Cursors are preserved 594 595 and Positions (Container) = Positions (Container)'Old 596 597 -- The actual value of other elements is preserved 598 599 and E.Equal_Except 600 (Elements (Container)'Old, 601 Elements (Container), 602 P.Get (Positions (Container), Find (Container, New_Item))), 603 604 -- Otherwise, New_Item is inserted in Container 605 606 others => 607 Length (Container) = Length (Container)'Old + 1 608 609 -- Other elements are preserved 610 611 and Model (Container)'Old <= Model (Container) 612 and M.Included_Except 613 (Model (Container), 614 Model (Container)'Old, 615 New_Item) 616 617 -- Mapping from cursors to elements is preserved 618 619 and Mapping_Preserved 620 (E_Left => Elements (Container)'Old, 621 E_Right => Elements (Container), 622 P_Left => Positions (Container)'Old, 623 P_Right => Positions (Container)) 624 and P.Keys_Included_Except 625 (Positions (Container), 626 Positions (Container)'Old, 627 Find (Container, New_Item))); 628 629 procedure Replace (Container : in out Set; New_Item : Element_Type) with 630 Global => null, 631 Pre => Contains (Container, New_Item), 632 Post => 633 634 -- Elements are preserved modulo equivalence 635 636 Model (Container) = Model (Container)'Old 637 and Contains (Container, New_Item) 638 639 -- Cursors are preserved 640 641 and Positions (Container) = Positions (Container)'Old 642 643 -- The element equivalent to New_Item in Container is replaced by 644 -- New_Item. 645 646 and Element (Container, Find (Container, New_Item)) = New_Item 647 and E.Equal_Except 648 (Elements (Container)'Old, 649 Elements (Container), 650 P.Get (Positions (Container), Find (Container, New_Item))); 651 652 procedure Exclude (Container : in out Set; Item : Element_Type) with 653 Global => null, 654 Post => not Contains (Container, Item), 655 Contract_Cases => 656 657 -- If Item is not in Container, nothing is changed 658 659 (not Contains (Container, Item) => 660 Model (Container) = Model (Container)'Old 661 and Elements (Container) = Elements (Container)'Old 662 and Positions (Container) = Positions (Container)'Old, 663 664 -- Otherwise, Item is removed from Container 665 666 others => 667 Length (Container) = Length (Container)'Old - 1 668 669 -- Other elements are preserved 670 671 and Model (Container) <= Model (Container)'Old 672 and M.Included_Except 673 (Model (Container)'Old, 674 Model (Container), 675 Item) 676 677 -- Mapping from cursors to elements is preserved 678 679 and Mapping_Preserved 680 (E_Left => Elements (Container), 681 E_Right => Elements (Container)'Old, 682 P_Left => Positions (Container), 683 P_Right => Positions (Container)'Old) 684 and P.Keys_Included_Except 685 (Positions (Container)'Old, 686 Positions (Container), 687 Find (Container, Item)'Old)); 688 689 procedure Delete (Container : in out Set; Item : Element_Type) with 690 Global => null, 691 Pre => Contains (Container, Item), 692 Post => 693 Length (Container) = Length (Container)'Old - 1 694 695 -- Item is no longer in Container 696 697 and not Contains (Container, Item) 698 699 -- Other elements are preserved 700 701 and Model (Container) <= Model (Container)'Old 702 and M.Included_Except 703 (Model (Container)'Old, 704 Model (Container), 705 Item) 706 707 -- Mapping from cursors to elements is preserved 708 709 and Mapping_Preserved 710 (E_Left => Elements (Container), 711 E_Right => Elements (Container)'Old, 712 P_Left => Positions (Container), 713 P_Right => Positions (Container)'Old) 714 and P.Keys_Included_Except 715 (Positions (Container)'Old, 716 Positions (Container), 717 Find (Container, Item)'Old); 718 719 procedure Delete (Container : in out Set; Position : in out Cursor) with 720 Global => null, 721 Pre => Has_Element (Container, Position), 722 Post => 723 Position = No_Element 724 and Length (Container) = Length (Container)'Old - 1 725 726 -- The element at position Position is no longer in Container 727 728 and not Contains (Container, Element (Container, Position)'Old) 729 and not P.Has_Key (Positions (Container), Position'Old) 730 731 -- Other elements are preserved 732 733 and Model (Container) <= Model (Container)'Old 734 and M.Included_Except 735 (Model (Container)'Old, 736 Model (Container), 737 Element (Container, Position)'Old) 738 739 -- Mapping from cursors to elements is preserved 740 741 and Mapping_Preserved 742 (E_Left => Elements (Container), 743 E_Right => Elements (Container)'Old, 744 P_Left => Positions (Container), 745 P_Right => Positions (Container)'Old) 746 and P.Keys_Included_Except 747 (Positions (Container)'Old, 748 Positions (Container), 749 Position'Old); 750 751 procedure Union (Target : in out Set; Source : Set) with 752 Global => null, 753 Pre => 754 Length (Source) - Length (Target and Source) <= 755 Target.Capacity - Length (Target), 756 Post => 757 Length (Target) = Length (Target)'Old 758 - M.Num_Overlaps (Model (Target)'Old, Model (Source)) 759 + Length (Source) 760 761 -- Elements already in Target are still in Target 762 763 and Model (Target)'Old <= Model (Target) 764 765 -- Elements of Source are included in Target 766 767 and Model (Source) <= Model (Target) 768 769 -- Elements of Target come from either Source or Target 770 771 and M.Included_In_Union 772 (Model (Target), Model (Source), Model (Target)'Old) 773 774 -- Actual value of elements come from either Left or Right 775 776 and E_Elements_Included 777 (Elements (Target), 778 Model (Target)'Old, 779 Elements (Target)'Old, 780 Elements (Source)) 781 782 and E_Elements_Included 783 (Elements (Target)'Old, Model (Target)'Old, Elements (Target)) 784 785 and E_Elements_Included 786 (Elements (Source), 787 Model (Target)'Old, 788 Elements (Source), 789 Elements (Target)) 790 791 -- Mapping from cursors of Target to elements is preserved 792 793 and Mapping_Preserved 794 (E_Left => Elements (Target)'Old, 795 E_Right => Elements (Target), 796 P_Left => Positions (Target)'Old, 797 P_Right => Positions (Target)); 798 799 function Union (Left, Right : Set) return Set with 800 Global => null, 801 Pre => Length (Left) <= Count_Type'Last - Length (Right), 802 Post => 803 Length (Union'Result) = Length (Left) 804 - M.Num_Overlaps (Model (Left), Model (Right)) 805 + Length (Right) 806 807 -- Elements of Left and Right are in the result of Union 808 809 and Model (Left) <= Model (Union'Result) 810 and Model (Right) <= Model (Union'Result) 811 812 -- Elements of the result of union come from either Left or Right 813 814 and 815 M.Included_In_Union 816 (Model (Union'Result), Model (Left), Model (Right)) 817 818 -- Actual value of elements come from either Left or Right 819 820 and E_Elements_Included 821 (Elements (Union'Result), 822 Model (Left), 823 Elements (Left), 824 Elements (Right)) 825 826 and E_Elements_Included 827 (Elements (Left), Model (Left), Elements (Union'Result)) 828 829 and E_Elements_Included 830 (Elements (Right), 831 Model (Left), 832 Elements (Right), 833 Elements (Union'Result)); 834 835 function "or" (Left, Right : Set) return Set renames Union; 836 837 procedure Intersection (Target : in out Set; Source : Set) with 838 Global => null, 839 Post => 840 Length (Target) = 841 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 842 843 -- Elements of Target were already in Target 844 845 and Model (Target) <= Model (Target)'Old 846 847 -- Elements of Target are in Source 848 849 and Model (Target) <= Model (Source) 850 851 -- Elements both in Source and Target are in the intersection 852 853 and M.Includes_Intersection 854 (Model (Target), Model (Source), Model (Target)'Old) 855 856 -- Actual value of elements of Target is preserved 857 858 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 859 and E_Elements_Included 860 (Elements (Target)'Old, Model (Source), Elements (Target)) 861 862 -- Mapping from cursors of Target to elements is preserved 863 864 and Mapping_Preserved 865 (E_Left => Elements (Target), 866 E_Right => Elements (Target)'Old, 867 P_Left => Positions (Target), 868 P_Right => Positions (Target)'Old); 869 870 function Intersection (Left, Right : Set) return Set with 871 Global => null, 872 Post => 873 Length (Intersection'Result) = 874 M.Num_Overlaps (Model (Left), Model (Right)) 875 876 -- Elements in the result of Intersection are in Left and Right 877 878 and Model (Intersection'Result) <= Model (Left) 879 and Model (Intersection'Result) <= Model (Right) 880 881 -- Elements both in Left and Right are in the result of Intersection 882 883 and M.Includes_Intersection 884 (Model (Intersection'Result), Model (Left), Model (Right)) 885 886 -- Actual value of elements come from Left 887 888 and E_Elements_Included 889 (Elements (Intersection'Result), Elements (Left)) 890 891 and E_Elements_Included 892 (Elements (Left), Model (Right), 893 Elements (Intersection'Result)); 894 895 function "and" (Left, Right : Set) return Set renames Intersection; 896 897 procedure Difference (Target : in out Set; Source : Set) with 898 Global => null, 899 Post => 900 Length (Target) = Length (Target)'Old - 901 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 902 903 -- Elements of Target were already in Target 904 905 and Model (Target) <= Model (Target)'Old 906 907 -- Elements of Target are not in Source 908 909 and M.No_Overlap (Model (Target), Model (Source)) 910 911 -- Elements in Target but not in Source are in the difference 912 913 and M.Included_In_Union 914 (Model (Target)'Old, Model (Target), Model (Source)) 915 916 -- Actual value of elements of Target is preserved 917 918 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 919 and E_Elements_Included 920 (Elements (Target)'Old, Model (Target), Elements (Target)) 921 922 -- Mapping from cursors of Target to elements is preserved 923 924 and Mapping_Preserved 925 (E_Left => Elements (Target), 926 E_Right => Elements (Target)'Old, 927 P_Left => Positions (Target), 928 P_Right => Positions (Target)'Old); 929 930 function Difference (Left, Right : Set) return Set with 931 Global => null, 932 Post => 933 Length (Difference'Result) = Length (Left) - 934 M.Num_Overlaps (Model (Left), Model (Right)) 935 936 -- Elements of the result of Difference are in Left 937 938 and Model (Difference'Result) <= Model (Left) 939 940 -- Elements of the result of Difference are in Right 941 942 and M.No_Overlap (Model (Difference'Result), Model (Right)) 943 944 -- Elements in Left but not in Right are in the difference 945 946 and M.Included_In_Union 947 (Model (Left), Model (Difference'Result), Model (Right)) 948 949 -- Actual value of elements come from Left 950 951 and E_Elements_Included 952 (Elements (Difference'Result), Elements (Left)) 953 954 and E_Elements_Included 955 (Elements (Left), 956 Model (Difference'Result), 957 Elements (Difference'Result)); 958 959 function "-" (Left, Right : Set) return Set renames Difference; 960 961 procedure Symmetric_Difference (Target : in out Set; Source : Set) with 962 Global => null, 963 Pre => 964 Length (Source) - Length (Target and Source) <= 965 Target.Capacity - Length (Target) + Length (Target and Source), 966 Post => 967 Length (Target) = Length (Target)'Old - 968 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + 969 Length (Source) 970 971 -- Elements of the difference were not both in Source and in Target 972 973 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source)) 974 975 -- Elements in Target but not in Source are in the difference 976 977 and M.Included_In_Union 978 (Model (Target)'Old, Model (Target), Model (Source)) 979 980 -- Elements in Source but not in Target are in the difference 981 982 and M.Included_In_Union 983 (Model (Source), Model (Target), Model (Target)'Old) 984 985 -- Actual value of elements come from either Left or Right 986 987 and E_Elements_Included 988 (Elements (Target), 989 Model (Target)'Old, 990 Elements (Target)'Old, 991 Elements (Source)) 992 993 and E_Elements_Included 994 (Elements (Target)'Old, Model (Target), Elements (Target)) 995 996 and E_Elements_Included 997 (Elements (Source), Model (Target), Elements (Target)); 998 999 function Symmetric_Difference (Left, Right : Set) return Set with 1000 Global => null, 1001 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1002 Post => 1003 Length (Symmetric_Difference'Result) = Length (Left) - 1004 2 * M.Num_Overlaps (Model (Left), Model (Right)) + 1005 Length (Right) 1006 1007 -- Elements of the difference were not both in Left and Right 1008 1009 and M.Not_In_Both 1010 (Model (Symmetric_Difference'Result), 1011 Model (Left), 1012 Model (Right)) 1013 1014 -- Elements in Left but not in Right are in the difference 1015 1016 and M.Included_In_Union 1017 (Model (Left), 1018 Model (Symmetric_Difference'Result), 1019 Model (Right)) 1020 1021 -- Elements in Right but not in Left are in the difference 1022 1023 and M.Included_In_Union 1024 (Model (Right), 1025 Model (Symmetric_Difference'Result), 1026 Model (Left)) 1027 1028 -- Actual value of elements come from either Left or Right 1029 1030 and E_Elements_Included 1031 (Elements (Symmetric_Difference'Result), 1032 Model (Left), 1033 Elements (Left), 1034 Elements (Right)) 1035 1036 and E_Elements_Included 1037 (Elements (Left), 1038 Model (Symmetric_Difference'Result), 1039 Elements (Symmetric_Difference'Result)) 1040 1041 and E_Elements_Included 1042 (Elements (Right), 1043 Model (Symmetric_Difference'Result), 1044 Elements (Symmetric_Difference'Result)); 1045 1046 function "xor" (Left, Right : Set) return Set 1047 renames Symmetric_Difference; 1048 1049 function Overlap (Left, Right : Set) return Boolean with 1050 Global => null, 1051 Post => 1052 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); 1053 1054 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with 1055 Global => null, 1056 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); 1057 1058 function First (Container : Set) return Cursor with 1059 Global => null, 1060 Contract_Cases => 1061 (Length (Container) = 0 => 1062 First'Result = No_Element, 1063 1064 others => 1065 Has_Element (Container, First'Result) 1066 and P.Get (Positions (Container), First'Result) = 1); 1067 1068 function Next (Container : Set; Position : Cursor) return Cursor with 1069 Global => null, 1070 Pre => 1071 Has_Element (Container, Position) or else Position = No_Element, 1072 Contract_Cases => 1073 (Position = No_Element 1074 or else P.Get (Positions (Container), Position) = Length (Container) 1075 => 1076 Next'Result = No_Element, 1077 1078 others => 1079 Has_Element (Container, Next'Result) 1080 and then P.Get (Positions (Container), Next'Result) = 1081 P.Get (Positions (Container), Position) + 1); 1082 1083 procedure Next (Container : Set; Position : in out Cursor) with 1084 Global => null, 1085 Pre => 1086 Has_Element (Container, Position) or else Position = No_Element, 1087 Contract_Cases => 1088 (Position = No_Element 1089 or else P.Get (Positions (Container), Position) = Length (Container) 1090 => 1091 Position = No_Element, 1092 1093 others => 1094 Has_Element (Container, Position) 1095 and then P.Get (Positions (Container), Position) = 1096 P.Get (Positions (Container), Position'Old) + 1); 1097 1098 function Find 1099 (Container : Set; 1100 Item : Element_Type) return Cursor 1101 with 1102 Global => null, 1103 Contract_Cases => 1104 1105 -- If Item is not contained in Container, Find returns No_Element 1106 1107 (not Contains (Model (Container), Item) => 1108 Find'Result = No_Element, 1109 1110 -- Otherwise, Find returns a valid cursor in Container 1111 1112 others => 1113 P.Has_Key (Positions (Container), Find'Result) 1114 and P.Get (Positions (Container), Find'Result) = 1115 Find (Elements (Container), Item) 1116 1117 -- The element designated by the result of Find is Item 1118 1119 and Equivalent_Elements 1120 (Element (Container, Find'Result), Item)); 1121 1122 function Contains (Container : Set; Item : Element_Type) return Boolean with 1123 Global => null, 1124 Post => Contains'Result = Contains (Model (Container), Item); 1125 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 1126 1127 function Has_Element (Container : Set; Position : Cursor) return Boolean 1128 with 1129 Global => null, 1130 Post => 1131 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1132 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1133 1134 function Default_Modulus (Capacity : Count_Type) return Hash_Type with 1135 Global => null; 1136 1137 generic 1138 type Key_Type (<>) is private; 1139 1140 with function Key (Element : Element_Type) return Key_Type; 1141 1142 with function Hash (Key : Key_Type) return Hash_Type; 1143 1144 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; 1145 1146 package Generic_Keys with SPARK_Mode is 1147 1148 package Formal_Model with Ghost is 1149 1150 function M_Included_Except 1151 (Left : M.Set; 1152 Right : M.Set; 1153 Key : Key_Type) return Boolean 1154 with 1155 Global => null, 1156 Post => 1157 M_Included_Except'Result = 1158 (for all E of Left => 1159 Contains (Right, E) 1160 or Equivalent_Keys (Generic_Keys.Key (E), Key)); 1161 1162 end Formal_Model; 1163 use Formal_Model; 1164 1165 function Key (Container : Set; Position : Cursor) return Key_Type with 1166 Global => null, 1167 Post => Key'Result = Key (Element (Container, Position)); 1168 pragma Annotate (GNATprove, Inline_For_Proof, Key); 1169 1170 function Element (Container : Set; Key : Key_Type) return Element_Type 1171 with 1172 Global => null, 1173 Pre => Contains (Container, Key), 1174 Post => 1175 Element'Result = Element (Container, Find (Container, Key)); 1176 pragma Annotate (GNATprove, Inline_For_Proof, Element); 1177 1178 procedure Replace 1179 (Container : in out Set; 1180 Key : Key_Type; 1181 New_Item : Element_Type) 1182 with 1183 Global => null, 1184 Pre => Contains (Container, Key), 1185 Post => 1186 Length (Container) = Length (Container)'Old 1187 1188 -- Key now maps to New_Item 1189 1190 and Element (Container, Key) = New_Item 1191 1192 -- New_Item is contained in Container 1193 1194 and Contains (Model (Container), New_Item) 1195 1196 -- Other elements are preserved 1197 1198 and M_Included_Except 1199 (Model (Container)'Old, 1200 Model (Container), 1201 Key) 1202 and M.Included_Except 1203 (Model (Container), 1204 Model (Container)'Old, 1205 New_Item) 1206 1207 -- Mapping from cursors to elements is preserved 1208 1209 and Mapping_Preserved_Except 1210 (E_Left => Elements (Container)'Old, 1211 E_Right => Elements (Container), 1212 P_Left => Positions (Container)'Old, 1213 P_Right => Positions (Container), 1214 Position => Find (Container, Key)) 1215 and Positions (Container) = Positions (Container)'Old; 1216 1217 procedure Exclude (Container : in out Set; Key : Key_Type) with 1218 Global => null, 1219 Post => not Contains (Container, Key), 1220 Contract_Cases => 1221 1222 -- If Key is not in Container, nothing is changed 1223 1224 (not Contains (Container, Key) => 1225 Model (Container) = Model (Container)'Old 1226 and Elements (Container) = Elements (Container)'Old 1227 and Positions (Container) = Positions (Container)'Old, 1228 1229 -- Otherwise, Key is removed from Container 1230 1231 others => 1232 Length (Container) = Length (Container)'Old - 1 1233 1234 -- Other elements are preserved 1235 1236 and Model (Container) <= Model (Container)'Old 1237 and M_Included_Except 1238 (Model (Container)'Old, 1239 Model (Container), 1240 Key) 1241 1242 -- Mapping from cursors to elements is preserved 1243 1244 and Mapping_Preserved 1245 (E_Left => Elements (Container), 1246 E_Right => Elements (Container)'Old, 1247 P_Left => Positions (Container), 1248 P_Right => Positions (Container)'Old) 1249 and P.Keys_Included_Except 1250 (Positions (Container)'Old, 1251 Positions (Container), 1252 Find (Container, Key)'Old)); 1253 1254 procedure Delete (Container : in out Set; Key : Key_Type) with 1255 Global => null, 1256 Pre => Contains (Container, Key), 1257 Post => 1258 Length (Container) = Length (Container)'Old - 1 1259 1260 -- Key is no longer in Container 1261 1262 and not Contains (Container, Key) 1263 1264 -- Other elements are preserved 1265 1266 and Model (Container) <= Model (Container)'Old 1267 and M_Included_Except 1268 (Model (Container)'Old, 1269 Model (Container), 1270 Key) 1271 1272 -- Mapping from cursors to elements is preserved 1273 1274 and Mapping_Preserved 1275 (E_Left => Elements (Container), 1276 E_Right => Elements (Container)'Old, 1277 P_Left => Positions (Container), 1278 P_Right => Positions (Container)'Old) 1279 and P.Keys_Included_Except 1280 (Positions (Container)'Old, 1281 Positions (Container), 1282 Find (Container, Key)'Old); 1283 1284 function Find (Container : Set; Key : Key_Type) return Cursor with 1285 Global => null, 1286 Contract_Cases => 1287 1288 -- If Key is not contained in Container, Find returns No_Element 1289 1290 ((for all E of Model (Container) => 1291 not Equivalent_Keys (Key, Generic_Keys.Key (E))) => 1292 Find'Result = No_Element, 1293 1294 -- Otherwise, Find returns a valid cursor in Container 1295 1296 others => 1297 P.Has_Key (Positions (Container), Find'Result) 1298 1299 -- The key designated by the result of Find is Key 1300 1301 and Equivalent_Keys 1302 (Generic_Keys.Key (Container, Find'Result), Key)); 1303 1304 function Contains (Container : Set; Key : Key_Type) return Boolean with 1305 Global => null, 1306 Post => 1307 Contains'Result = 1308 (for some E of Model (Container) => 1309 Equivalent_Keys (Key, Generic_Keys.Key (E))); 1310 1311 end Generic_Keys; 1312 1313private 1314 pragma SPARK_Mode (Off); 1315 1316 pragma Inline (Next); 1317 1318 type Node_Type is 1319 record 1320 Element : Element_Type; 1321 Next : Count_Type; 1322 Has_Element : Boolean := False; 1323 end record; 1324 1325 package HT_Types is new 1326 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); 1327 1328 type Set (Capacity : Count_Type; Modulus : Hash_Type) is 1329 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; 1330 1331 use HT_Types; 1332 1333 Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>); 1334 1335end Ada.Containers.Formal_Hashed_Sets; 1336