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