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 _ O R D E R E D _ S E T S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2020, 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_Ordered_Sets in 33-- the 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: Key, Element, Next, Query_Element, Previous, 42-- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the 43-- need to have cursors which are valid on different containers (typically 44-- a 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. The operators "<" and ">" that could not be modified that way 47-- have been removed. 48 49with Ada.Containers.Functional_Maps; 50with Ada.Containers.Functional_Sets; 51with Ada.Containers.Functional_Vectors; 52private with Ada.Containers.Red_Black_Trees; 53 54generic 55 type Element_Type is private; 56 57 with function "<" (Left, Right : Element_Type) return Boolean is <>; 58 59package Ada.Containers.Formal_Ordered_Sets with 60 SPARK_Mode 61is 62 pragma Annotate (CodePeer, Skip_Analysis); 63 64 function Equivalent_Elements (Left, Right : Element_Type) return Boolean 65 with 66 Global => null, 67 Post => 68 Equivalent_Elements'Result = 69 (not (Left < Right) and not (Right < Left)); 70 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements); 71 72 type Set (Capacity : Count_Type) is private with 73 Iterable => (First => First, 74 Next => Next, 75 Has_Element => Has_Element, 76 Element => Element), 77 Default_Initial_Condition => Is_Empty (Set); 78 pragma Preelaborable_Initialization (Set); 79 80 type Cursor is record 81 Node : Count_Type; 82 end record; 83 84 No_Element : constant Cursor := (Node => 0); 85 86 function Length (Container : Set) return Count_Type with 87 Global => null, 88 Post => Length'Result <= Container.Capacity; 89 90 pragma Unevaluated_Use_Of_Old (Allow); 91 92 package Formal_Model with Ghost is 93 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; 94 95 package M is new Ada.Containers.Functional_Sets 96 (Element_Type => Element_Type, 97 Equivalent_Elements => Equivalent_Elements); 98 99 function "=" 100 (Left : M.Set; 101 Right : M.Set) return Boolean renames M."="; 102 103 function "<=" 104 (Left : M.Set; 105 Right : M.Set) return Boolean renames M."<="; 106 107 package E is new Ada.Containers.Functional_Vectors 108 (Element_Type => Element_Type, 109 Index_Type => Positive_Count_Type); 110 111 function "=" 112 (Left : E.Sequence; 113 Right : E.Sequence) return Boolean renames E."="; 114 115 function "<" 116 (Left : E.Sequence; 117 Right : E.Sequence) return Boolean renames E."<"; 118 119 function "<=" 120 (Left : E.Sequence; 121 Right : E.Sequence) return Boolean renames E."<="; 122 123 function E_Bigger_Than_Range 124 (Container : E.Sequence; 125 Fst : Positive_Count_Type; 126 Lst : Count_Type; 127 Item : Element_Type) return Boolean 128 with 129 Global => null, 130 Pre => Lst <= E.Length (Container), 131 Post => 132 E_Bigger_Than_Range'Result = 133 (for all I in Fst .. Lst => E.Get (Container, I) < Item); 134 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range); 135 136 function E_Smaller_Than_Range 137 (Container : E.Sequence; 138 Fst : Positive_Count_Type; 139 Lst : Count_Type; 140 Item : Element_Type) return Boolean 141 with 142 Global => null, 143 Pre => Lst <= E.Length (Container), 144 Post => 145 E_Smaller_Than_Range'Result = 146 (for all I in Fst .. Lst => Item < E.Get (Container, I)); 147 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range); 148 149 function E_Is_Find 150 (Container : E.Sequence; 151 Item : Element_Type; 152 Position : Count_Type) return Boolean 153 with 154 Global => null, 155 Pre => Position - 1 <= E.Length (Container), 156 Post => 157 E_Is_Find'Result = 158 159 ((if Position > 0 then 160 E_Bigger_Than_Range (Container, 1, Position - 1, Item)) 161 162 and (if Position < E.Length (Container) then 163 E_Smaller_Than_Range 164 (Container, 165 Position + 1, 166 E.Length (Container), 167 Item))); 168 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find); 169 170 function Find 171 (Container : E.Sequence; 172 Item : Element_Type) return Count_Type 173 -- Search for Item in Container 174 175 with 176 Global => null, 177 Post => 178 (if Find'Result > 0 then 179 Find'Result <= E.Length (Container) 180 and Equivalent_Elements (Item, E.Get (Container, Find'Result))); 181 182 function E_Elements_Included 183 (Left : E.Sequence; 184 Right : E.Sequence) return Boolean 185 -- The elements of Left are contained in Right 186 187 with 188 Global => null, 189 Post => 190 E_Elements_Included'Result = 191 (for all I in 1 .. E.Length (Left) => 192 Find (Right, E.Get (Left, I)) > 0 193 and then E.Get (Right, Find (Right, E.Get (Left, I))) = 194 E.Get (Left, I)); 195 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 196 197 function E_Elements_Included 198 (Left : E.Sequence; 199 Model : M.Set; 200 Right : E.Sequence) return Boolean 201 -- The elements of Container contained in Model are in Right 202 203 with 204 Global => null, 205 Post => 206 E_Elements_Included'Result = 207 (for all I in 1 .. E.Length (Left) => 208 (if M.Contains (Model, E.Get (Left, I)) then 209 Find (Right, E.Get (Left, I)) > 0 210 and then E.Get (Right, Find (Right, E.Get (Left, I))) = 211 E.Get (Left, I))); 212 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 213 214 function E_Elements_Included 215 (Container : E.Sequence; 216 Model : M.Set; 217 Left : E.Sequence; 218 Right : E.Sequence) return Boolean 219 -- The elements of Container contained in Model are in Left and others 220 -- are in Right. 221 222 with 223 Global => null, 224 Post => 225 E_Elements_Included'Result = 226 (for all I in 1 .. E.Length (Container) => 227 (if M.Contains (Model, E.Get (Container, I)) then 228 Find (Left, E.Get (Container, I)) > 0 229 and then E.Get (Left, Find (Left, E.Get (Container, I))) = 230 E.Get (Container, I) 231 else 232 Find (Right, E.Get (Container, I)) > 0 233 and then E.Get (Right, Find (Right, E.Get (Container, I))) = 234 E.Get (Container, I))); 235 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); 236 237 package P is new Ada.Containers.Functional_Maps 238 (Key_Type => Cursor, 239 Element_Type => Positive_Count_Type, 240 Equivalent_Keys => "=", 241 Enable_Handling_Of_Equivalence => False); 242 243 function "=" 244 (Left : P.Map; 245 Right : P.Map) return Boolean renames P."="; 246 247 function "<=" 248 (Left : P.Map; 249 Right : P.Map) return Boolean renames P."<="; 250 251 function P_Positions_Shifted 252 (Small : P.Map; 253 Big : P.Map; 254 Cut : Positive_Count_Type; 255 Count : Count_Type := 1) return Boolean 256 with 257 Global => null, 258 Post => 259 P_Positions_Shifted'Result = 260 261 -- Big contains all cursors of Small 262 263 (P.Keys_Included (Small, Big) 264 265 -- Cursors located before Cut are not moved, cursors located 266 -- after are shifted by Count. 267 268 and (for all I of Small => 269 (if P.Get (Small, I) < Cut then 270 P.Get (Big, I) = P.Get (Small, I) 271 else 272 P.Get (Big, I) - Count = P.Get (Small, I))) 273 274 -- New cursors of Big (if any) are between Cut and Cut - 1 + 275 -- Count. 276 277 and (for all I of Big => 278 P.Has_Key (Small, I) 279 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); 280 281 function Mapping_Preserved 282 (E_Left : E.Sequence; 283 E_Right : E.Sequence; 284 P_Left : P.Map; 285 P_Right : P.Map) return Boolean 286 with 287 Ghost, 288 Global => null, 289 Post => 290 (if Mapping_Preserved'Result then 291 292 -- Right contains all the cursors of Left 293 294 P.Keys_Included (P_Left, P_Right) 295 296 -- Right contains all the elements of Left 297 298 and E_Elements_Included (E_Left, E_Right) 299 300 -- Mappings from cursors to elements induced by E_Left, P_Left 301 -- and E_Right, P_Right are the same. 302 303 and (for all C of P_Left => 304 E.Get (E_Left, P.Get (P_Left, C)) = 305 E.Get (E_Right, P.Get (P_Right, C)))); 306 307 function Mapping_Preserved_Except 308 (E_Left : E.Sequence; 309 E_Right : E.Sequence; 310 P_Left : P.Map; 311 P_Right : P.Map; 312 Position : Cursor) return Boolean 313 with 314 Ghost, 315 Global => null, 316 Post => 317 (if Mapping_Preserved_Except'Result then 318 319 -- Right contains all the cursors of Left 320 321 P.Keys_Included (P_Left, P_Right) 322 323 -- Mappings from cursors to elements induced by E_Left, P_Left 324 -- and E_Right, P_Right are the same except for Position. 325 326 and (for all C of P_Left => 327 (if C /= Position then 328 E.Get (E_Left, P.Get (P_Left, C)) = 329 E.Get (E_Right, P.Get (P_Right, C))))); 330 331 function Model (Container : Set) return M.Set with 332 -- The high-level model of a set is a set of elements. Neither cursors 333 -- nor order of elements are represented in this model. Elements are 334 -- modeled up to equivalence. 335 336 Ghost, 337 Global => null, 338 Post => M.Length (Model'Result) = Length (Container); 339 340 function Elements (Container : Set) return E.Sequence with 341 -- The Elements sequence represents the underlying list structure of 342 -- sets that is used for iteration. It stores the actual values of 343 -- elements in the set. It does not model cursors. 344 345 Ghost, 346 Global => null, 347 Post => 348 E.Length (Elements'Result) = Length (Container) 349 350 -- It only contains keys contained in Model 351 352 and (for all Item of Elements'Result => 353 M.Contains (Model (Container), Item)) 354 355 -- It contains all the elements contained in Model 356 357 and (for all Item of Model (Container) => 358 (Find (Elements'Result, Item) > 0 359 and then Equivalent_Elements 360 (E.Get (Elements'Result, Find (Elements'Result, Item)), 361 Item))) 362 363 -- It is sorted in increasing order 364 365 and (for all I in 1 .. Length (Container) => 366 Find (Elements'Result, E.Get (Elements'Result, I)) = I 367 and 368 E_Is_Find 369 (Elements'Result, E.Get (Elements'Result, I), I)); 370 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements); 371 372 function Positions (Container : Set) return P.Map with 373 -- The Positions map is used to model cursors. It only contains valid 374 -- cursors and maps them to their position in the container. 375 376 Ghost, 377 Global => null, 378 Post => 379 not P.Has_Key (Positions'Result, No_Element) 380 381 -- Positions of cursors are smaller than the container's length 382 383 and then 384 (for all I of Positions'Result => 385 P.Get (Positions'Result, I) in 1 .. Length (Container) 386 387 -- No two cursors have the same position. Note that we do not 388 -- state that there is a cursor in the map for each position, as 389 -- it is rarely needed. 390 391 and then 392 (for all J of Positions'Result => 393 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) 394 then I = J))); 395 396 procedure Lift_Abstraction_Level (Container : Set) with 397 -- Lift_Abstraction_Level is a ghost procedure that does nothing but 398 -- assume that we can access the same elements by iterating over 399 -- positions or cursors. 400 -- This information is not generally useful except when switching from 401 -- a low-level, cursor-aware view of a container, to a high-level, 402 -- position-based view. 403 404 Ghost, 405 Global => null, 406 Post => 407 (for all Item of Elements (Container) => 408 (for some I of Positions (Container) => 409 E.Get (Elements (Container), P.Get (Positions (Container), I)) = 410 Item)); 411 412 function Contains 413 (C : M.Set; 414 K : Element_Type) return Boolean renames M.Contains; 415 -- To improve readability of contracts, we rename the function used to 416 -- search for an element in the model to Contains. 417 418 end Formal_Model; 419 use Formal_Model; 420 421 Empty_Set : constant Set; 422 423 function "=" (Left, Right : Set) return Boolean with 424 Global => null, 425 Post => 426 427 -- If two sets are equal, they contain the same elements in the same 428 -- order. 429 430 (if "="'Result then Elements (Left) = Elements (Right) 431 432 -- If they are different, then they do not contain the same elements 433 434 else 435 not E_Elements_Included (Elements (Left), Elements (Right)) 436 or not E_Elements_Included (Elements (Right), Elements (Left))); 437 438 function Equivalent_Sets (Left, Right : Set) return Boolean with 439 Global => null, 440 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right)); 441 442 function To_Set (New_Item : Element_Type) return Set with 443 Global => null, 444 Post => 445 M.Is_Singleton (Model (To_Set'Result), New_Item) 446 and Length (To_Set'Result) = 1 447 and E.Get (Elements (To_Set'Result), 1) = New_Item; 448 449 function Is_Empty (Container : Set) return Boolean with 450 Global => null, 451 Post => Is_Empty'Result = (Length (Container) = 0); 452 453 procedure Clear (Container : in out Set) with 454 Global => null, 455 Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); 456 457 procedure Assign (Target : in out Set; Source : Set) with 458 Global => null, 459 Pre => Target.Capacity >= Length (Source), 460 Post => 461 Model (Target) = Model (Source) 462 and Elements (Target) = Elements (Source) 463 and Length (Target) = Length (Source); 464 465 function Copy (Source : Set; Capacity : Count_Type := 0) return Set with 466 Global => null, 467 Pre => Capacity = 0 or else Capacity >= Source.Capacity, 468 Post => 469 Model (Copy'Result) = Model (Source) 470 and Elements (Copy'Result) = Elements (Source) 471 and Positions (Copy'Result) = Positions (Source) 472 and (if Capacity = 0 then 473 Copy'Result.Capacity = Source.Capacity 474 else 475 Copy'Result.Capacity = Capacity); 476 477 function Element 478 (Container : Set; 479 Position : Cursor) return Element_Type 480 with 481 Global => null, 482 Pre => Has_Element (Container, Position), 483 Post => 484 Element'Result = 485 E.Get (Elements (Container), P.Get (Positions (Container), Position)); 486 pragma Annotate (GNATprove, Inline_For_Proof, Element); 487 488 procedure Replace_Element 489 (Container : in out Set; 490 Position : Cursor; 491 New_Item : Element_Type) 492 with 493 Global => null, 494 Pre => Has_Element (Container, Position), 495 Post => 496 Length (Container) = Length (Container)'Old 497 498 -- Position now maps to New_Item 499 500 and Element (Container, Position) = New_Item 501 502 -- New_Item is contained in Container 503 504 and Contains (Model (Container), New_Item) 505 506 -- Other elements are preserved 507 508 and M.Included_Except 509 (Model (Container)'Old, 510 Model (Container), 511 Element (Container, Position)'Old) 512 and M.Included_Except 513 (Model (Container), 514 Model (Container)'Old, 515 New_Item) 516 517 -- Mapping from cursors to elements is preserved 518 519 and Mapping_Preserved_Except 520 (E_Left => Elements (Container)'Old, 521 E_Right => Elements (Container), 522 P_Left => Positions (Container)'Old, 523 P_Right => Positions (Container), 524 Position => Position) 525 and Positions (Container) = Positions (Container)'Old; 526 527 procedure Move (Target : in out Set; Source : in out Set) with 528 Global => null, 529 Pre => Target.Capacity >= Length (Source), 530 Post => 531 Model (Target) = Model (Source)'Old 532 and Elements (Target) = Elements (Source)'Old 533 and Length (Source)'Old = Length (Target) 534 and Length (Source) = 0; 535 536 procedure Insert 537 (Container : in out Set; 538 New_Item : Element_Type; 539 Position : out Cursor; 540 Inserted : out Boolean) 541 with 542 Global => null, 543 Pre => 544 Length (Container) < Container.Capacity 545 or Contains (Container, New_Item), 546 Post => 547 Contains (Container, New_Item) 548 and Has_Element (Container, Position) 549 and Equivalent_Elements (Element (Container, Position), New_Item) 550 and E_Is_Find 551 (Elements (Container), 552 New_Item, 553 P.Get (Positions (Container), Position)), 554 Contract_Cases => 555 556 -- If New_Item is already in Container, it is not modified and Inserted 557 -- is set to False. 558 559 (Contains (Container, New_Item) => 560 not Inserted 561 and Model (Container) = Model (Container)'Old 562 and Elements (Container) = Elements (Container)'Old 563 and Positions (Container) = Positions (Container)'Old, 564 565 -- Otherwise, New_Item is inserted in Container and Inserted is set to 566 -- True 567 568 others => 569 Inserted 570 and Length (Container) = Length (Container)'Old + 1 571 572 -- Position now maps to New_Item 573 574 and Element (Container, Position) = New_Item 575 576 -- Other elements are preserved 577 578 and Model (Container)'Old <= Model (Container) 579 and M.Included_Except 580 (Model (Container), 581 Model (Container)'Old, 582 New_Item) 583 584 -- The elements of Container located before Position are preserved 585 586 and E.Range_Equal 587 (Left => Elements (Container)'Old, 588 Right => Elements (Container), 589 Fst => 1, 590 Lst => P.Get (Positions (Container), Position) - 1) 591 592 -- Other elements are shifted by 1 593 594 and E.Range_Shifted 595 (Left => Elements (Container)'Old, 596 Right => Elements (Container), 597 Fst => P.Get (Positions (Container), Position), 598 Lst => Length (Container)'Old, 599 Offset => 1) 600 601 -- A new cursor has been inserted at position Position in 602 -- Container. 603 604 and P_Positions_Shifted 605 (Positions (Container)'Old, 606 Positions (Container), 607 Cut => P.Get (Positions (Container), Position))); 608 609 procedure Insert 610 (Container : in out Set; 611 New_Item : Element_Type) 612 with 613 Global => null, 614 Pre => 615 Length (Container) < Container.Capacity 616 and then (not Contains (Container, New_Item)), 617 Post => 618 Length (Container) = Length (Container)'Old + 1 619 and Contains (Container, New_Item) 620 621 -- New_Item is inserted in the set 622 623 and E.Get (Elements (Container), 624 Find (Elements (Container), New_Item)) = New_Item 625 626 -- Other mappings are preserved 627 628 and Model (Container)'Old <= Model (Container) 629 and M.Included_Except 630 (Model (Container), 631 Model (Container)'Old, 632 New_Item) 633 634 -- The elements of Container located before New_Item are preserved 635 636 and E.Range_Equal 637 (Left => Elements (Container)'Old, 638 Right => Elements (Container), 639 Fst => 1, 640 Lst => Find (Elements (Container), New_Item) - 1) 641 642 -- Other elements are shifted by 1 643 644 and E.Range_Shifted 645 (Left => Elements (Container)'Old, 646 Right => Elements (Container), 647 Fst => Find (Elements (Container), New_Item), 648 Lst => Length (Container)'Old, 649 Offset => 1) 650 651 -- A new cursor has been inserted in Container 652 653 and P_Positions_Shifted 654 (Positions (Container)'Old, 655 Positions (Container), 656 Cut => Find (Elements (Container), New_Item)); 657 658 procedure Include 659 (Container : in out Set; 660 New_Item : Element_Type) 661 with 662 Global => null, 663 Pre => 664 Length (Container) < Container.Capacity 665 or Contains (Container, New_Item), 666 Post => Contains (Container, New_Item), 667 Contract_Cases => 668 669 -- If New_Item is already in Container 670 671 (Contains (Container, New_Item) => 672 673 -- Elements are preserved 674 675 Model (Container)'Old = Model (Container) 676 677 -- Cursors are preserved 678 679 and Positions (Container) = Positions (Container)'Old 680 681 -- The element equivalent to New_Item in Container is replaced by 682 -- New_Item. 683 684 and E.Get (Elements (Container), 685 Find (Elements (Container), New_Item)) = New_Item 686 687 and E.Equal_Except 688 (Elements (Container)'Old, 689 Elements (Container), 690 Find (Elements (Container), New_Item)), 691 692 -- Otherwise, New_Item is inserted in Container 693 694 others => 695 Length (Container) = Length (Container)'Old + 1 696 697 -- Other elements are preserved 698 699 and Model (Container)'Old <= Model (Container) 700 and M.Included_Except 701 (Model (Container), 702 Model (Container)'Old, 703 New_Item) 704 705 -- New_Item is inserted in Container 706 707 and E.Get (Elements (Container), 708 Find (Elements (Container), New_Item)) = New_Item 709 710 -- The Elements of Container located before New_Item are preserved 711 712 and E.Range_Equal 713 (Left => Elements (Container)'Old, 714 Right => Elements (Container), 715 Fst => 1, 716 Lst => Find (Elements (Container), New_Item) - 1) 717 718 -- Other Elements are shifted by 1 719 720 and E.Range_Shifted 721 (Left => Elements (Container)'Old, 722 Right => Elements (Container), 723 Fst => Find (Elements (Container), New_Item), 724 Lst => Length (Container)'Old, 725 Offset => 1) 726 727 -- A new cursor has been inserted in Container 728 729 and P_Positions_Shifted 730 (Positions (Container)'Old, 731 Positions (Container), 732 Cut => Find (Elements (Container), New_Item))); 733 734 procedure Replace 735 (Container : in out Set; 736 New_Item : Element_Type) 737 with 738 Global => null, 739 Pre => Contains (Container, New_Item), 740 Post => 741 742 -- Elements are preserved 743 744 Model (Container)'Old = Model (Container) 745 746 -- Cursors are preserved 747 748 and Positions (Container) = Positions (Container)'Old 749 750 -- The element equivalent to New_Item in Container is replaced by 751 -- New_Item. 752 753 and E.Get (Elements (Container), 754 Find (Elements (Container), New_Item)) = New_Item 755 and E.Equal_Except 756 (Elements (Container)'Old, 757 Elements (Container), 758 Find (Elements (Container), New_Item)); 759 760 procedure Exclude 761 (Container : in out Set; 762 Item : Element_Type) 763 with 764 Global => null, 765 Post => not Contains (Container, Item), 766 Contract_Cases => 767 768 -- If Item is not in Container, nothing is changed 769 770 (not Contains (Container, Item) => 771 Model (Container) = Model (Container)'Old 772 and Elements (Container) = Elements (Container)'Old 773 and Positions (Container) = Positions (Container)'Old, 774 775 -- Otherwise, Item is removed from Container 776 777 others => 778 Length (Container) = Length (Container)'Old - 1 779 780 -- Other elements are preserved 781 782 and Model (Container) <= Model (Container)'Old 783 and M.Included_Except 784 (Model (Container)'Old, 785 Model (Container), 786 Item) 787 788 -- The elements of Container located before Item are preserved 789 790 and E.Range_Equal 791 (Left => Elements (Container)'Old, 792 Right => Elements (Container), 793 Fst => 1, 794 Lst => Find (Elements (Container), Item)'Old - 1) 795 796 -- The elements located after Item are shifted by 1 797 798 and E.Range_Shifted 799 (Left => Elements (Container), 800 Right => Elements (Container)'Old, 801 Fst => Find (Elements (Container), Item)'Old, 802 Lst => Length (Container), 803 Offset => 1) 804 805 -- A cursor has been removed from Container 806 807 and P_Positions_Shifted 808 (Positions (Container), 809 Positions (Container)'Old, 810 Cut => Find (Elements (Container), Item)'Old)); 811 812 procedure Delete 813 (Container : in out Set; 814 Item : Element_Type) 815 with 816 Global => null, 817 Pre => Contains (Container, Item), 818 Post => 819 Length (Container) = Length (Container)'Old - 1 820 821 -- Item is no longer in Container 822 823 and not Contains (Container, Item) 824 825 -- Other elements are preserved 826 827 and Model (Container) <= Model (Container)'Old 828 and M.Included_Except 829 (Model (Container)'Old, 830 Model (Container), 831 Item) 832 833 -- The elements of Container located before Item are preserved 834 835 and E.Range_Equal 836 (Left => Elements (Container)'Old, 837 Right => Elements (Container), 838 Fst => 1, 839 Lst => Find (Elements (Container), Item)'Old - 1) 840 841 -- The elements located after Item are shifted by 1 842 843 and E.Range_Shifted 844 (Left => Elements (Container), 845 Right => Elements (Container)'Old, 846 Fst => Find (Elements (Container), Item)'Old, 847 Lst => Length (Container), 848 Offset => 1) 849 850 -- A cursor has been removed from Container 851 852 and P_Positions_Shifted 853 (Positions (Container), 854 Positions (Container)'Old, 855 Cut => Find (Elements (Container), Item)'Old); 856 857 procedure Delete 858 (Container : in out Set; 859 Position : in out Cursor) 860 with 861 Global => null, 862 Depends => (Container =>+ Position, Position => null), 863 Pre => Has_Element (Container, Position), 864 Post => 865 Position = No_Element 866 and Length (Container) = Length (Container)'Old - 1 867 868 -- The element at position Position is no longer in Container 869 870 and not Contains (Container, Element (Container, Position)'Old) 871 and not P.Has_Key (Positions (Container), Position'Old) 872 873 -- Other elements are preserved 874 875 and Model (Container) <= Model (Container)'Old 876 and M.Included_Except 877 (Model (Container)'Old, 878 Model (Container), 879 Element (Container, Position)'Old) 880 881 -- The elements of Container located before Position are preserved. 882 883 and E.Range_Equal 884 (Left => Elements (Container)'Old, 885 Right => Elements (Container), 886 Fst => 1, 887 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) 888 889 -- The elements located after Position are shifted by 1 890 891 and E.Range_Shifted 892 (Left => Elements (Container), 893 Right => Elements (Container)'Old, 894 Fst => P.Get (Positions (Container)'Old, Position'Old), 895 Lst => Length (Container), 896 Offset => 1) 897 898 -- Position has been removed from Container 899 900 and P_Positions_Shifted 901 (Positions (Container), 902 Positions (Container)'Old, 903 Cut => P.Get (Positions (Container)'Old, Position'Old)); 904 905 procedure Delete_First (Container : in out Set) with 906 Global => null, 907 Contract_Cases => 908 (Length (Container) = 0 => Length (Container) = 0, 909 others => 910 Length (Container) = Length (Container)'Old - 1 911 912 -- The first element has been removed from Container 913 914 and not Contains (Container, First_Element (Container)'Old) 915 916 -- Other elements are preserved 917 918 and Model (Container) <= Model (Container)'Old 919 and M.Included_Except 920 (Model (Container)'Old, 921 Model (Container), 922 First_Element (Container)'Old) 923 924 -- Other elements are shifted by 1 925 926 and E.Range_Shifted 927 (Left => Elements (Container), 928 Right => Elements (Container)'Old, 929 Fst => 1, 930 Lst => Length (Container), 931 Offset => 1) 932 933 -- First has been removed from Container 934 935 and P_Positions_Shifted 936 (Positions (Container), 937 Positions (Container)'Old, 938 Cut => 1)); 939 940 procedure Delete_Last (Container : in out Set) with 941 Global => null, 942 Contract_Cases => 943 (Length (Container) = 0 => Length (Container) = 0, 944 others => 945 Length (Container) = Length (Container)'Old - 1 946 947 -- The last element has been removed from Container 948 949 and not Contains (Container, Last_Element (Container)'Old) 950 951 -- Other elements are preserved 952 953 and Model (Container) <= Model (Container)'Old 954 and M.Included_Except 955 (Model (Container)'Old, 956 Model (Container), 957 Last_Element (Container)'Old) 958 959 -- Others elements of Container are preserved 960 961 and E.Range_Equal 962 (Left => Elements (Container)'Old, 963 Right => Elements (Container), 964 Fst => 1, 965 Lst => Length (Container)) 966 967 -- Last cursor has been removed from Container 968 969 and Positions (Container) <= Positions (Container)'Old); 970 971 procedure Union (Target : in out Set; Source : Set) with 972 Global => null, 973 Pre => 974 Length (Source) - Length (Target and Source) <= 975 Target.Capacity - Length (Target), 976 Post => 977 Length (Target) = Length (Target)'Old 978 - M.Num_Overlaps (Model (Target)'Old, Model (Source)) 979 + Length (Source) 980 981 -- Elements already in Target are still in Target 982 983 and Model (Target)'Old <= Model (Target) 984 985 -- Elements of Source are included in Target 986 987 and Model (Source) <= Model (Target) 988 989 -- Elements of Target come from either Source or Target 990 991 and 992 M.Included_In_Union 993 (Model (Target), Model (Source), Model (Target)'Old) 994 995 -- Actual value of elements come from either Left or Right 996 997 and 998 E_Elements_Included 999 (Elements (Target), 1000 Model (Target)'Old, 1001 Elements (Target)'Old, 1002 Elements (Source)) 1003 and 1004 E_Elements_Included 1005 (Elements (Target)'Old, Model (Target)'Old, Elements (Target)) 1006 and 1007 E_Elements_Included 1008 (Elements (Source), 1009 Model (Target)'Old, 1010 Elements (Source), 1011 Elements (Target)) 1012 1013 -- Mapping from cursors of Target to elements is preserved 1014 1015 and Mapping_Preserved 1016 (E_Left => Elements (Target)'Old, 1017 E_Right => Elements (Target), 1018 P_Left => Positions (Target)'Old, 1019 P_Right => Positions (Target)); 1020 1021 function Union (Left, Right : Set) return Set with 1022 Global => null, 1023 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1024 Post => 1025 Length (Union'Result) = Length (Left) 1026 - M.Num_Overlaps (Model (Left), Model (Right)) 1027 + Length (Right) 1028 1029 -- Elements of Left and Right are in the result of Union 1030 1031 and Model (Left) <= Model (Union'Result) 1032 and Model (Right) <= Model (Union'Result) 1033 1034 -- Elements of the result of union come from either Left or Right 1035 1036 and 1037 M.Included_In_Union 1038 (Model (Union'Result), Model (Left), Model (Right)) 1039 1040 -- Actual value of elements come from either Left or Right 1041 1042 and 1043 E_Elements_Included 1044 (Elements (Union'Result), 1045 Model (Left), 1046 Elements (Left), 1047 Elements (Right)) 1048 and 1049 E_Elements_Included 1050 (Elements (Left), Model (Left), Elements (Union'Result)) 1051 and 1052 E_Elements_Included 1053 (Elements (Right), 1054 Model (Left), 1055 Elements (Right), 1056 Elements (Union'Result)); 1057 1058 function "or" (Left, Right : Set) return Set renames Union; 1059 1060 procedure Intersection (Target : in out Set; Source : Set) with 1061 Global => null, 1062 Post => 1063 Length (Target) = 1064 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 1065 1066 -- Elements of Target were already in Target 1067 1068 and Model (Target) <= Model (Target)'Old 1069 1070 -- Elements of Target are in Source 1071 1072 and Model (Target) <= Model (Source) 1073 1074 -- Elements both in Source and Target are in the intersection 1075 1076 and 1077 M.Includes_Intersection 1078 (Model (Target), Model (Source), Model (Target)'Old) 1079 1080 -- Actual value of elements of Target is preserved 1081 1082 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 1083 and 1084 E_Elements_Included 1085 (Elements (Target)'Old, Model (Source), Elements (Target)) 1086 1087 -- Mapping from cursors of Target to elements is preserved 1088 1089 and Mapping_Preserved 1090 (E_Left => Elements (Target), 1091 E_Right => Elements (Target)'Old, 1092 P_Left => Positions (Target), 1093 P_Right => Positions (Target)'Old); 1094 1095 function Intersection (Left, Right : Set) return Set with 1096 Global => null, 1097 Post => 1098 Length (Intersection'Result) = 1099 M.Num_Overlaps (Model (Left), Model (Right)) 1100 1101 -- Elements in the result of Intersection are in Left and Right 1102 1103 and Model (Intersection'Result) <= Model (Left) 1104 and Model (Intersection'Result) <= Model (Right) 1105 1106 -- Elements both in Left and Right are in the result of Intersection 1107 1108 and 1109 M.Includes_Intersection 1110 (Model (Intersection'Result), Model (Left), Model (Right)) 1111 1112 -- Actual value of elements come from Left 1113 1114 and 1115 E_Elements_Included 1116 (Elements (Intersection'Result), Elements (Left)) 1117 and 1118 E_Elements_Included 1119 (Elements (Left), Model (Right), Elements (Intersection'Result)); 1120 1121 function "and" (Left, Right : Set) return Set renames Intersection; 1122 1123 procedure Difference (Target : in out Set; Source : Set) with 1124 Global => null, 1125 Post => 1126 Length (Target) = Length (Target)'Old - 1127 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 1128 1129 -- Elements of Target were already in Target 1130 1131 and Model (Target) <= Model (Target)'Old 1132 1133 -- Elements of Target are not in Source 1134 1135 and M.No_Overlap (Model (Target), Model (Source)) 1136 1137 -- Elements in Target but not in Source are in the difference 1138 1139 and 1140 M.Included_In_Union 1141 (Model (Target)'Old, Model (Target), Model (Source)) 1142 1143 -- Actual value of elements of Target is preserved 1144 1145 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 1146 and 1147 E_Elements_Included 1148 (Elements (Target)'Old, Model (Target), Elements (Target)) 1149 1150 -- Mapping from cursors of Target to elements is preserved 1151 1152 and Mapping_Preserved 1153 (E_Left => Elements (Target), 1154 E_Right => Elements (Target)'Old, 1155 P_Left => Positions (Target), 1156 P_Right => Positions (Target)'Old); 1157 1158 function Difference (Left, Right : Set) return Set with 1159 Global => null, 1160 Post => 1161 Length (Difference'Result) = Length (Left) - 1162 M.Num_Overlaps (Model (Left), Model (Right)) 1163 1164 -- Elements of the result of Difference are in Left 1165 1166 and Model (Difference'Result) <= Model (Left) 1167 1168 -- Elements of the result of Difference are in Right 1169 1170 and M.No_Overlap (Model (Difference'Result), Model (Right)) 1171 1172 -- Elements in Left but not in Right are in the difference 1173 1174 and 1175 M.Included_In_Union 1176 (Model (Left), Model (Difference'Result), Model (Right)) 1177 1178 -- Actual value of elements come from Left 1179 1180 and 1181 E_Elements_Included (Elements (Difference'Result), Elements (Left)) 1182 and 1183 E_Elements_Included 1184 (Elements (Left), 1185 Model (Difference'Result), 1186 Elements (Difference'Result)); 1187 1188 function "-" (Left, Right : Set) return Set renames Difference; 1189 1190 procedure Symmetric_Difference (Target : in out Set; Source : Set) with 1191 Global => null, 1192 Pre => 1193 Length (Source) - Length (Target and Source) <= 1194 Target.Capacity - Length (Target) + Length (Target and Source), 1195 Post => 1196 Length (Target) = Length (Target)'Old - 1197 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + 1198 Length (Source) 1199 1200 -- Elements of the difference were not both in Source and in Target 1201 1202 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source)) 1203 1204 -- Elements in Target but not in Source are in the difference 1205 1206 and 1207 M.Included_In_Union 1208 (Model (Target)'Old, Model (Target), Model (Source)) 1209 1210 -- Elements in Source but not in Target are in the difference 1211 1212 and 1213 M.Included_In_Union 1214 (Model (Source), Model (Target), Model (Target)'Old) 1215 1216 -- Actual value of elements come from either Left or Right 1217 1218 and 1219 E_Elements_Included 1220 (Elements (Target), 1221 Model (Target)'Old, 1222 Elements (Target)'Old, 1223 Elements (Source)) 1224 and 1225 E_Elements_Included 1226 (Elements (Target)'Old, Model (Target), Elements (Target)) 1227 and 1228 E_Elements_Included 1229 (Elements (Source), Model (Target), Elements (Target)); 1230 1231 function Symmetric_Difference (Left, Right : Set) return Set with 1232 Global => null, 1233 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1234 Post => 1235 Length (Symmetric_Difference'Result) = Length (Left) - 1236 2 * M.Num_Overlaps (Model (Left), Model (Right)) + 1237 Length (Right) 1238 1239 -- Elements of the difference were not both in Left and Right 1240 1241 and 1242 M.Not_In_Both 1243 (Model (Symmetric_Difference'Result), Model (Left), Model (Right)) 1244 1245 -- Elements in Left but not in Right are in the difference 1246 1247 and 1248 M.Included_In_Union 1249 (Model (Left), Model (Symmetric_Difference'Result), Model (Right)) 1250 1251 -- Elements in Right but not in Left are in the difference 1252 1253 and 1254 M.Included_In_Union 1255 (Model (Right), Model (Symmetric_Difference'Result), Model (Left)) 1256 1257 -- Actual value of elements come from either Left or Right 1258 1259 and 1260 E_Elements_Included 1261 (Elements (Symmetric_Difference'Result), 1262 Model (Left), 1263 Elements (Left), 1264 Elements (Right)) 1265 and 1266 E_Elements_Included 1267 (Elements (Left), 1268 Model (Symmetric_Difference'Result), 1269 Elements (Symmetric_Difference'Result)) 1270 and 1271 E_Elements_Included 1272 (Elements (Right), 1273 Model (Symmetric_Difference'Result), 1274 Elements (Symmetric_Difference'Result)); 1275 1276 function "xor" (Left, Right : Set) return Set 1277 renames Symmetric_Difference; 1278 1279 function Overlap (Left, Right : Set) return Boolean with 1280 Global => null, 1281 Post => 1282 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); 1283 1284 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with 1285 Global => null, 1286 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); 1287 1288 function First (Container : Set) return Cursor with 1289 Global => null, 1290 Contract_Cases => 1291 (Length (Container) = 0 => 1292 First'Result = No_Element, 1293 1294 others => 1295 Has_Element (Container, First'Result) 1296 and P.Get (Positions (Container), First'Result) = 1); 1297 1298 function First_Element (Container : Set) return Element_Type with 1299 Global => null, 1300 Pre => not Is_Empty (Container), 1301 Post => 1302 First_Element'Result = E.Get (Elements (Container), 1) 1303 and E_Smaller_Than_Range 1304 (Elements (Container), 1305 2, 1306 Length (Container), 1307 First_Element'Result); 1308 1309 function Last (Container : Set) return Cursor with 1310 Global => null, 1311 Contract_Cases => 1312 (Length (Container) = 0 => 1313 Last'Result = No_Element, 1314 1315 others => 1316 Has_Element (Container, Last'Result) 1317 and P.Get (Positions (Container), Last'Result) = 1318 Length (Container)); 1319 1320 function Last_Element (Container : Set) return Element_Type with 1321 Global => null, 1322 Pre => not Is_Empty (Container), 1323 Post => 1324 Last_Element'Result = E.Get (Elements (Container), Length (Container)) 1325 and E_Bigger_Than_Range 1326 (Elements (Container), 1327 1, 1328 Length (Container) - 1, 1329 Last_Element'Result); 1330 1331 function Next (Container : Set; Position : Cursor) return Cursor with 1332 Global => null, 1333 Pre => 1334 Has_Element (Container, Position) or else Position = No_Element, 1335 Contract_Cases => 1336 (Position = No_Element 1337 or else P.Get (Positions (Container), Position) = Length (Container) 1338 => 1339 Next'Result = No_Element, 1340 1341 others => 1342 Has_Element (Container, Next'Result) 1343 and then P.Get (Positions (Container), Next'Result) = 1344 P.Get (Positions (Container), Position) + 1); 1345 1346 procedure Next (Container : Set; Position : in out Cursor) with 1347 Global => null, 1348 Pre => 1349 Has_Element (Container, Position) or else Position = No_Element, 1350 Contract_Cases => 1351 (Position = No_Element 1352 or else P.Get (Positions (Container), Position) = Length (Container) 1353 => 1354 Position = No_Element, 1355 1356 others => 1357 Has_Element (Container, Position) 1358 and then P.Get (Positions (Container), Position) = 1359 P.Get (Positions (Container), Position'Old) + 1); 1360 1361 function Previous (Container : Set; Position : Cursor) return Cursor with 1362 Global => null, 1363 Pre => 1364 Has_Element (Container, Position) or else Position = No_Element, 1365 Contract_Cases => 1366 (Position = No_Element 1367 or else P.Get (Positions (Container), Position) = 1 1368 => 1369 Previous'Result = No_Element, 1370 1371 others => 1372 Has_Element (Container, Previous'Result) 1373 and then P.Get (Positions (Container), Previous'Result) = 1374 P.Get (Positions (Container), Position) - 1); 1375 1376 procedure Previous (Container : Set; Position : in out Cursor) with 1377 Global => null, 1378 Pre => 1379 Has_Element (Container, Position) or else Position = No_Element, 1380 Contract_Cases => 1381 (Position = No_Element 1382 or else P.Get (Positions (Container), Position) = 1 1383 => 1384 Position = No_Element, 1385 1386 others => 1387 Has_Element (Container, Position) 1388 and then P.Get (Positions (Container), Position) = 1389 P.Get (Positions (Container), Position'Old) - 1); 1390 1391 function Find (Container : Set; Item : Element_Type) return Cursor with 1392 Global => null, 1393 Contract_Cases => 1394 1395 -- If Item is not contained in Container, Find returns No_Element 1396 1397 (not Contains (Model (Container), Item) => 1398 not P.Has_Key (Positions (Container), Find'Result) 1399 and Find'Result = No_Element, 1400 1401 -- Otherwise, Find returns a valid cursor in Container 1402 1403 others => 1404 P.Has_Key (Positions (Container), Find'Result) 1405 and P.Get (Positions (Container), Find'Result) = 1406 Find (Elements (Container), Item) 1407 1408 -- The element designated by the result of Find is Item 1409 1410 and Equivalent_Elements 1411 (Element (Container, Find'Result), Item)); 1412 1413 function Floor (Container : Set; Item : Element_Type) return Cursor with 1414 Global => null, 1415 Contract_Cases => 1416 (Length (Container) = 0 or else Item < First_Element (Container) => 1417 Floor'Result = No_Element, 1418 others => 1419 Has_Element (Container, Floor'Result) 1420 and 1421 not (Item < E.Get (Elements (Container), 1422 P.Get (Positions (Container), Floor'Result))) 1423 and E_Is_Find 1424 (Elements (Container), 1425 Item, 1426 P.Get (Positions (Container), Floor'Result))); 1427 1428 function Ceiling (Container : Set; Item : Element_Type) return Cursor with 1429 Global => null, 1430 Contract_Cases => 1431 (Length (Container) = 0 or else Last_Element (Container) < Item => 1432 Ceiling'Result = No_Element, 1433 others => 1434 Has_Element (Container, Ceiling'Result) 1435 and 1436 not (E.Get (Elements (Container), 1437 P.Get (Positions (Container), Ceiling'Result)) < 1438 Item) 1439 and E_Is_Find 1440 (Elements (Container), 1441 Item, 1442 P.Get (Positions (Container), Ceiling'Result))); 1443 1444 function Contains (Container : Set; Item : Element_Type) return Boolean with 1445 Global => null, 1446 Post => Contains'Result = Contains (Model (Container), Item); 1447 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 1448 1449 function Has_Element (Container : Set; Position : Cursor) return Boolean 1450 with 1451 Global => null, 1452 Post => 1453 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1454 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1455 1456 generic 1457 type Key_Type (<>) is private; 1458 1459 with function Key (Element : Element_Type) return Key_Type; 1460 1461 with function "<" (Left, Right : Key_Type) return Boolean is <>; 1462 1463 package Generic_Keys with SPARK_Mode is 1464 1465 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with 1466 Global => null, 1467 Post => 1468 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left)); 1469 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys); 1470 1471 package Formal_Model with Ghost is 1472 function E_Bigger_Than_Range 1473 (Container : E.Sequence; 1474 Fst : Positive_Count_Type; 1475 Lst : Count_Type; 1476 Key : Key_Type) return Boolean 1477 with 1478 Global => null, 1479 Pre => Lst <= E.Length (Container), 1480 Post => 1481 E_Bigger_Than_Range'Result = 1482 (for all I in Fst .. Lst => 1483 Generic_Keys.Key (E.Get (Container, I)) < Key); 1484 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range); 1485 1486 function E_Smaller_Than_Range 1487 (Container : E.Sequence; 1488 Fst : Positive_Count_Type; 1489 Lst : Count_Type; 1490 Key : Key_Type) return Boolean 1491 with 1492 Global => null, 1493 Pre => Lst <= E.Length (Container), 1494 Post => 1495 E_Smaller_Than_Range'Result = 1496 (for all I in Fst .. Lst => 1497 Key < Generic_Keys.Key (E.Get (Container, I))); 1498 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range); 1499 1500 function E_Is_Find 1501 (Container : E.Sequence; 1502 Key : Key_Type; 1503 Position : Count_Type) return Boolean 1504 with 1505 Global => null, 1506 Pre => Position - 1 <= E.Length (Container), 1507 Post => 1508 E_Is_Find'Result = 1509 1510 ((if Position > 0 then 1511 E_Bigger_Than_Range (Container, 1, Position - 1, Key)) 1512 1513 and (if Position < E.Length (Container) then 1514 E_Smaller_Than_Range 1515 (Container, 1516 Position + 1, 1517 E.Length (Container), 1518 Key))); 1519 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find); 1520 1521 function Find 1522 (Container : E.Sequence; 1523 Key : Key_Type) return Count_Type 1524 -- Search for Key in Container 1525 1526 with 1527 Global => null, 1528 Post => 1529 (if Find'Result > 0 then 1530 Find'Result <= E.Length (Container) 1531 and Equivalent_Keys 1532 (Key, Generic_Keys.Key (E.Get (Container, Find'Result))) 1533 and E_Is_Find (Container, Key, Find'Result)); 1534 1535 function M_Included_Except 1536 (Left : M.Set; 1537 Right : M.Set; 1538 Key : Key_Type) return Boolean 1539 with 1540 Global => null, 1541 Post => 1542 M_Included_Except'Result = 1543 (for all E of Left => 1544 Contains (Right, E) 1545 or Equivalent_Keys (Generic_Keys.Key (E), Key)); 1546 end Formal_Model; 1547 use Formal_Model; 1548 1549 function Key (Container : Set; Position : Cursor) return Key_Type with 1550 Global => null, 1551 Post => Key'Result = Key (Element (Container, Position)); 1552 pragma Annotate (GNATprove, Inline_For_Proof, Key); 1553 1554 function Element (Container : Set; Key : Key_Type) return Element_Type 1555 with 1556 Global => null, 1557 Pre => Contains (Container, Key), 1558 Post => 1559 Element'Result = Element (Container, Find (Container, Key)); 1560 pragma Annotate (GNATprove, Inline_For_Proof, Element); 1561 1562 procedure Replace 1563 (Container : in out Set; 1564 Key : Key_Type; 1565 New_Item : Element_Type) 1566 with 1567 Global => null, 1568 Pre => Contains (Container, Key), 1569 Post => 1570 Length (Container) = Length (Container)'Old 1571 1572 -- Key now maps to New_Item 1573 1574 and Element (Container, Key) = New_Item 1575 1576 -- New_Item is contained in Container 1577 1578 and Contains (Model (Container), New_Item) 1579 1580 -- Other elements are preserved 1581 1582 and M_Included_Except 1583 (Model (Container)'Old, 1584 Model (Container), 1585 Key) 1586 and M.Included_Except 1587 (Model (Container), 1588 Model (Container)'Old, 1589 New_Item) 1590 1591 -- Mapping from cursors to elements is preserved 1592 1593 and Mapping_Preserved_Except 1594 (E_Left => Elements (Container)'Old, 1595 E_Right => Elements (Container), 1596 P_Left => Positions (Container)'Old, 1597 P_Right => Positions (Container), 1598 Position => Find (Container, Key)) 1599 and Positions (Container) = Positions (Container)'Old; 1600 1601 procedure Exclude (Container : in out Set; Key : Key_Type) with 1602 Global => null, 1603 Post => not Contains (Container, Key), 1604 Contract_Cases => 1605 1606 -- If Key is not in Container, nothing is changed 1607 1608 (not Contains (Container, Key) => 1609 Model (Container) = Model (Container)'Old 1610 and Elements (Container) = Elements (Container)'Old 1611 and Positions (Container) = Positions (Container)'Old, 1612 1613 -- Otherwise, Key is removed from Container 1614 1615 others => 1616 Length (Container) = Length (Container)'Old - 1 1617 1618 -- Other elements are preserved 1619 1620 and Model (Container) <= Model (Container)'Old 1621 and M_Included_Except 1622 (Model (Container)'Old, 1623 Model (Container), 1624 Key) 1625 1626 -- The elements of Container located before Key are preserved 1627 1628 and E.Range_Equal 1629 (Left => Elements (Container)'Old, 1630 Right => Elements (Container), 1631 Fst => 1, 1632 Lst => Find (Elements (Container), Key)'Old - 1) 1633 1634 -- The elements located after Key are shifted by 1 1635 1636 and E.Range_Shifted 1637 (Left => Elements (Container), 1638 Right => Elements (Container)'Old, 1639 Fst => Find (Elements (Container), Key)'Old, 1640 Lst => Length (Container), 1641 Offset => 1) 1642 1643 -- A cursor has been removed from Container 1644 1645 and P_Positions_Shifted 1646 (Positions (Container), 1647 Positions (Container)'Old, 1648 Cut => Find (Elements (Container), Key)'Old)); 1649 1650 procedure Delete (Container : in out Set; Key : Key_Type) with 1651 Global => null, 1652 Pre => Contains (Container, Key), 1653 Post => 1654 Length (Container) = Length (Container)'Old - 1 1655 1656 -- Key is no longer in Container 1657 1658 and not Contains (Container, Key) 1659 1660 -- Other elements are preserved 1661 1662 and Model (Container) <= Model (Container)'Old 1663 and M_Included_Except 1664 (Model (Container)'Old, 1665 Model (Container), 1666 Key) 1667 1668 -- The elements of Container located before Key are preserved 1669 1670 and E.Range_Equal 1671 (Left => Elements (Container)'Old, 1672 Right => Elements (Container), 1673 Fst => 1, 1674 Lst => Find (Elements (Container), Key)'Old - 1) 1675 1676 -- The elements located after Key are shifted by 1 1677 1678 and E.Range_Shifted 1679 (Left => Elements (Container), 1680 Right => Elements (Container)'Old, 1681 Fst => Find (Elements (Container), Key)'Old, 1682 Lst => Length (Container), 1683 Offset => 1) 1684 1685 -- A cursor has been removed from Container 1686 1687 and P_Positions_Shifted 1688 (Positions (Container), 1689 Positions (Container)'Old, 1690 Cut => Find (Elements (Container), Key)'Old); 1691 1692 function Find (Container : Set; Key : Key_Type) return Cursor with 1693 Global => null, 1694 Contract_Cases => 1695 1696 -- If Key is not contained in Container, Find returns No_Element 1697 1698 ((for all E of Model (Container) => 1699 not Equivalent_Keys (Key, Generic_Keys.Key (E))) => 1700 not P.Has_Key (Positions (Container), Find'Result) 1701 and Find'Result = No_Element, 1702 1703 -- Otherwise, Find returns a valid cursor in Container 1704 1705 others => 1706 P.Has_Key (Positions (Container), Find'Result) 1707 and P.Get (Positions (Container), Find'Result) = 1708 Find (Elements (Container), Key) 1709 1710 -- The element designated by the result of Find is Key 1711 1712 and Equivalent_Keys 1713 (Generic_Keys.Key (Element (Container, Find'Result)), Key)); 1714 1715 function Floor (Container : Set; Key : Key_Type) return Cursor with 1716 Global => null, 1717 Contract_Cases => 1718 (Length (Container) = 0 1719 or else Key < Generic_Keys.Key (First_Element (Container)) => 1720 Floor'Result = No_Element, 1721 others => 1722 Has_Element (Container, Floor'Result) 1723 and 1724 not (Key < 1725 Generic_Keys.Key 1726 (E.Get (Elements (Container), 1727 P.Get (Positions (Container), Floor'Result)))) 1728 and E_Is_Find 1729 (Elements (Container), 1730 Key, 1731 P.Get (Positions (Container), Floor'Result))); 1732 1733 function Ceiling (Container : Set; Key : Key_Type) return Cursor with 1734 Global => null, 1735 Contract_Cases => 1736 (Length (Container) = 0 1737 or else Generic_Keys.Key (Last_Element (Container)) < Key => 1738 Ceiling'Result = No_Element, 1739 others => 1740 Has_Element (Container, Ceiling'Result) 1741 and 1742 not (Generic_Keys.Key 1743 (E.Get (Elements (Container), 1744 P.Get (Positions (Container), Ceiling'Result))) 1745 < Key) 1746 and E_Is_Find 1747 (Elements (Container), 1748 Key, 1749 P.Get (Positions (Container), Ceiling'Result))); 1750 1751 function Contains (Container : Set; Key : Key_Type) return Boolean with 1752 Global => null, 1753 Post => 1754 Contains'Result = 1755 (for some E of Model (Container) => 1756 Equivalent_Keys (Key, Generic_Keys.Key (E))); 1757 1758 end Generic_Keys; 1759 1760private 1761 pragma SPARK_Mode (Off); 1762 1763 pragma Inline (Next); 1764 pragma Inline (Previous); 1765 1766 type Node_Type is record 1767 Has_Element : Boolean := False; 1768 Parent : Count_Type := 0; 1769 Left : Count_Type := 0; 1770 Right : Count_Type := 0; 1771 Color : Red_Black_Trees.Color_Type; 1772 Element : Element_Type; 1773 end record; 1774 1775 package Tree_Types is 1776 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); 1777 1778 type Set (Capacity : Count_Type) is 1779 new Tree_Types.Tree_Type (Capacity) with null record; 1780 1781 use Red_Black_Trees; 1782 1783 Empty_Set : constant Set := (Capacity => 0, others => <>); 1784 1785end Ada.Containers.Formal_Ordered_Sets; 1786