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-2018, Free Software Foundation, Inc. -- 10-- -- 11-- This specification is derived from the Ada Reference Manual for use with -- 12-- GNAT. The copyright notice above, and the license provisions that follow -- 13-- apply solely to the contents of the part following the private keyword. -- 14-- -- 15-- GNAT is free software; you can redistribute it and/or modify it under -- 16-- terms of the GNU General Public License as published by the Free Soft- -- 17-- ware Foundation; either version 3, or (at your option) any later ver- -- 18-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 19-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 20-- or FITNESS FOR A PARTICULAR PURPOSE. -- 21-- -- 22-- As a special exception under Section 7 of GPL version 3, you are granted -- 23-- additional permissions described in the GCC Runtime Library Exception, -- 24-- version 3.1, as published by the Free Software Foundation. -- 25-- -- 26-- You should have received a copy of the GNU General Public License and -- 27-- a copy of the GCC Runtime Library Exception along with this program; -- 28-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 29-- <http://www.gnu.org/licenses/>. -- 30------------------------------------------------------------------------------ 31 32-- This spec is derived from package Ada.Containers.Bounded_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 Pre => Has_Element (Container, Position), 863 Post => 864 Position = No_Element 865 and Length (Container) = Length (Container)'Old - 1 866 867 -- The element at position Position is no longer in Container 868 869 and not Contains (Container, Element (Container, Position)'Old) 870 and not P.Has_Key (Positions (Container), Position'Old) 871 872 -- Other elements are preserved 873 874 and Model (Container) <= Model (Container)'Old 875 and M.Included_Except 876 (Model (Container)'Old, 877 Model (Container), 878 Element (Container, Position)'Old) 879 880 -- The elements of Container located before Position are preserved. 881 882 and E.Range_Equal 883 (Left => Elements (Container)'Old, 884 Right => Elements (Container), 885 Fst => 1, 886 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) 887 888 -- The elements located after Position are shifted by 1 889 890 and E.Range_Shifted 891 (Left => Elements (Container), 892 Right => Elements (Container)'Old, 893 Fst => P.Get (Positions (Container)'Old, Position'Old), 894 Lst => Length (Container), 895 Offset => 1) 896 897 -- Position has been removed from Container 898 899 and P_Positions_Shifted 900 (Positions (Container), 901 Positions (Container)'Old, 902 Cut => P.Get (Positions (Container)'Old, Position'Old)); 903 904 procedure Delete_First (Container : in out Set) with 905 Global => null, 906 Contract_Cases => 907 (Length (Container) = 0 => Length (Container) = 0, 908 others => 909 Length (Container) = Length (Container)'Old - 1 910 911 -- The first element has been removed from Container 912 913 and not Contains (Container, First_Element (Container)'Old) 914 915 -- Other elements are preserved 916 917 and Model (Container) <= Model (Container)'Old 918 and M.Included_Except 919 (Model (Container)'Old, 920 Model (Container), 921 First_Element (Container)'Old) 922 923 -- Other elements are shifted by 1 924 925 and E.Range_Shifted 926 (Left => Elements (Container), 927 Right => Elements (Container)'Old, 928 Fst => 1, 929 Lst => Length (Container), 930 Offset => 1) 931 932 -- First has been removed from Container 933 934 and P_Positions_Shifted 935 (Positions (Container), 936 Positions (Container)'Old, 937 Cut => 1)); 938 939 procedure Delete_Last (Container : in out Set) with 940 Global => null, 941 Contract_Cases => 942 (Length (Container) = 0 => Length (Container) = 0, 943 others => 944 Length (Container) = Length (Container)'Old - 1 945 946 -- The last element has been removed from Container 947 948 and not Contains (Container, Last_Element (Container)'Old) 949 950 -- Other elements are preserved 951 952 and Model (Container) <= Model (Container)'Old 953 and M.Included_Except 954 (Model (Container)'Old, 955 Model (Container), 956 Last_Element (Container)'Old) 957 958 -- Others elements of Container are preserved 959 960 and E.Range_Equal 961 (Left => Elements (Container)'Old, 962 Right => Elements (Container), 963 Fst => 1, 964 Lst => Length (Container)) 965 966 -- Last cursor has been removed from Container 967 968 and Positions (Container) <= Positions (Container)'Old); 969 970 procedure Union (Target : in out Set; Source : Set) with 971 Global => null, 972 Pre => 973 Length (Source) - Length (Target and Source) <= 974 Target.Capacity - Length (Target), 975 Post => 976 Length (Target) = Length (Target)'Old 977 - M.Num_Overlaps (Model (Target)'Old, Model (Source)) 978 + Length (Source) 979 980 -- Elements already in Target are still in Target 981 982 and Model (Target)'Old <= Model (Target) 983 984 -- Elements of Source are included in Target 985 986 and Model (Source) <= Model (Target) 987 988 -- Elements of Target come from either Source or Target 989 990 and 991 M.Included_In_Union 992 (Model (Target), Model (Source), Model (Target)'Old) 993 994 -- Actual value of elements come from either Left or Right 995 996 and 997 E_Elements_Included 998 (Elements (Target), 999 Model (Target)'Old, 1000 Elements (Target)'Old, 1001 Elements (Source)) 1002 and 1003 E_Elements_Included 1004 (Elements (Target)'Old, Model (Target)'Old, Elements (Target)) 1005 and 1006 E_Elements_Included 1007 (Elements (Source), 1008 Model (Target)'Old, 1009 Elements (Source), 1010 Elements (Target)) 1011 1012 -- Mapping from cursors of Target to elements is preserved 1013 1014 and Mapping_Preserved 1015 (E_Left => Elements (Target)'Old, 1016 E_Right => Elements (Target), 1017 P_Left => Positions (Target)'Old, 1018 P_Right => Positions (Target)); 1019 1020 function Union (Left, Right : Set) return Set with 1021 Global => null, 1022 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1023 Post => 1024 Length (Union'Result) = Length (Left) 1025 - M.Num_Overlaps (Model (Left), Model (Right)) 1026 + Length (Right) 1027 1028 -- Elements of Left and Right are in the result of Union 1029 1030 and Model (Left) <= Model (Union'Result) 1031 and Model (Right) <= Model (Union'Result) 1032 1033 -- Elements of the result of union come from either Left or Right 1034 1035 and 1036 M.Included_In_Union 1037 (Model (Union'Result), Model (Left), Model (Right)) 1038 1039 -- Actual value of elements come from either Left or Right 1040 1041 and 1042 E_Elements_Included 1043 (Elements (Union'Result), 1044 Model (Left), 1045 Elements (Left), 1046 Elements (Right)) 1047 and 1048 E_Elements_Included 1049 (Elements (Left), Model (Left), Elements (Union'Result)) 1050 and 1051 E_Elements_Included 1052 (Elements (Right), 1053 Model (Left), 1054 Elements (Right), 1055 Elements (Union'Result)); 1056 1057 function "or" (Left, Right : Set) return Set renames Union; 1058 1059 procedure Intersection (Target : in out Set; Source : Set) with 1060 Global => null, 1061 Post => 1062 Length (Target) = 1063 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 1064 1065 -- Elements of Target were already in Target 1066 1067 and Model (Target) <= Model (Target)'Old 1068 1069 -- Elements of Target are in Source 1070 1071 and Model (Target) <= Model (Source) 1072 1073 -- Elements both in Source and Target are in the intersection 1074 1075 and 1076 M.Includes_Intersection 1077 (Model (Target), Model (Source), Model (Target)'Old) 1078 1079 -- Actual value of elements of Target is preserved 1080 1081 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 1082 and 1083 E_Elements_Included 1084 (Elements (Target)'Old, Model (Source), Elements (Target)) 1085 1086 -- Mapping from cursors of Target to elements is preserved 1087 1088 and Mapping_Preserved 1089 (E_Left => Elements (Target), 1090 E_Right => Elements (Target)'Old, 1091 P_Left => Positions (Target), 1092 P_Right => Positions (Target)'Old); 1093 1094 function Intersection (Left, Right : Set) return Set with 1095 Global => null, 1096 Post => 1097 Length (Intersection'Result) = 1098 M.Num_Overlaps (Model (Left), Model (Right)) 1099 1100 -- Elements in the result of Intersection are in Left and Right 1101 1102 and Model (Intersection'Result) <= Model (Left) 1103 and Model (Intersection'Result) <= Model (Right) 1104 1105 -- Elements both in Left and Right are in the result of Intersection 1106 1107 and 1108 M.Includes_Intersection 1109 (Model (Intersection'Result), Model (Left), Model (Right)) 1110 1111 -- Actual value of elements come from Left 1112 1113 and 1114 E_Elements_Included 1115 (Elements (Intersection'Result), Elements (Left)) 1116 and 1117 E_Elements_Included 1118 (Elements (Left), Model (Right), Elements (Intersection'Result)); 1119 1120 function "and" (Left, Right : Set) return Set renames Intersection; 1121 1122 procedure Difference (Target : in out Set; Source : Set) with 1123 Global => null, 1124 Post => 1125 Length (Target) = Length (Target)'Old - 1126 M.Num_Overlaps (Model (Target)'Old, Model (Source)) 1127 1128 -- Elements of Target were already in Target 1129 1130 and Model (Target) <= Model (Target)'Old 1131 1132 -- Elements of Target are not in Source 1133 1134 and M.No_Overlap (Model (Target), Model (Source)) 1135 1136 -- Elements in Target but not in Source are in the difference 1137 1138 and 1139 M.Included_In_Union 1140 (Model (Target)'Old, Model (Target), Model (Source)) 1141 1142 -- Actual value of elements of Target is preserved 1143 1144 and E_Elements_Included (Elements (Target), Elements (Target)'Old) 1145 and 1146 E_Elements_Included 1147 (Elements (Target)'Old, Model (Target), Elements (Target)) 1148 1149 -- Mapping from cursors of Target to elements is preserved 1150 1151 and Mapping_Preserved 1152 (E_Left => Elements (Target), 1153 E_Right => Elements (Target)'Old, 1154 P_Left => Positions (Target), 1155 P_Right => Positions (Target)'Old); 1156 1157 function Difference (Left, Right : Set) return Set with 1158 Global => null, 1159 Post => 1160 Length (Difference'Result) = Length (Left) - 1161 M.Num_Overlaps (Model (Left), Model (Right)) 1162 1163 -- Elements of the result of Difference are in Left 1164 1165 and Model (Difference'Result) <= Model (Left) 1166 1167 -- Elements of the result of Difference are in Right 1168 1169 and M.No_Overlap (Model (Difference'Result), Model (Right)) 1170 1171 -- Elements in Left but not in Right are in the difference 1172 1173 and 1174 M.Included_In_Union 1175 (Model (Left), Model (Difference'Result), Model (Right)) 1176 1177 -- Actual value of elements come from Left 1178 1179 and 1180 E_Elements_Included (Elements (Difference'Result), Elements (Left)) 1181 and 1182 E_Elements_Included 1183 (Elements (Left), 1184 Model (Difference'Result), 1185 Elements (Difference'Result)); 1186 1187 function "-" (Left, Right : Set) return Set renames Difference; 1188 1189 procedure Symmetric_Difference (Target : in out Set; Source : Set) with 1190 Global => null, 1191 Pre => 1192 Length (Source) - Length (Target and Source) <= 1193 Target.Capacity - Length (Target) + Length (Target and Source), 1194 Post => 1195 Length (Target) = Length (Target)'Old - 1196 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + 1197 Length (Source) 1198 1199 -- Elements of the difference were not both in Source and in Target 1200 1201 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source)) 1202 1203 -- Elements in Target but not in Source are in the difference 1204 1205 and 1206 M.Included_In_Union 1207 (Model (Target)'Old, Model (Target), Model (Source)) 1208 1209 -- Elements in Source but not in Target are in the difference 1210 1211 and 1212 M.Included_In_Union 1213 (Model (Source), Model (Target), Model (Target)'Old) 1214 1215 -- Actual value of elements come from either Left or Right 1216 1217 and 1218 E_Elements_Included 1219 (Elements (Target), 1220 Model (Target)'Old, 1221 Elements (Target)'Old, 1222 Elements (Source)) 1223 and 1224 E_Elements_Included 1225 (Elements (Target)'Old, Model (Target), Elements (Target)) 1226 and 1227 E_Elements_Included 1228 (Elements (Source), Model (Target), Elements (Target)); 1229 1230 function Symmetric_Difference (Left, Right : Set) return Set with 1231 Global => null, 1232 Pre => Length (Left) <= Count_Type'Last - Length (Right), 1233 Post => 1234 Length (Symmetric_Difference'Result) = Length (Left) - 1235 2 * M.Num_Overlaps (Model (Left), Model (Right)) + 1236 Length (Right) 1237 1238 -- Elements of the difference were not both in Left and Right 1239 1240 and 1241 M.Not_In_Both 1242 (Model (Symmetric_Difference'Result), Model (Left), Model (Right)) 1243 1244 -- Elements in Left but not in Right are in the difference 1245 1246 and 1247 M.Included_In_Union 1248 (Model (Left), Model (Symmetric_Difference'Result), Model (Right)) 1249 1250 -- Elements in Right but not in Left are in the difference 1251 1252 and 1253 M.Included_In_Union 1254 (Model (Right), Model (Symmetric_Difference'Result), Model (Left)) 1255 1256 -- Actual value of elements come from either Left or Right 1257 1258 and 1259 E_Elements_Included 1260 (Elements (Symmetric_Difference'Result), 1261 Model (Left), 1262 Elements (Left), 1263 Elements (Right)) 1264 and 1265 E_Elements_Included 1266 (Elements (Left), 1267 Model (Symmetric_Difference'Result), 1268 Elements (Symmetric_Difference'Result)) 1269 and 1270 E_Elements_Included 1271 (Elements (Right), 1272 Model (Symmetric_Difference'Result), 1273 Elements (Symmetric_Difference'Result)); 1274 1275 function "xor" (Left, Right : Set) return Set 1276 renames Symmetric_Difference; 1277 1278 function Overlap (Left, Right : Set) return Boolean with 1279 Global => null, 1280 Post => 1281 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); 1282 1283 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with 1284 Global => null, 1285 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); 1286 1287 function First (Container : Set) return Cursor with 1288 Global => null, 1289 Contract_Cases => 1290 (Length (Container) = 0 => 1291 First'Result = No_Element, 1292 1293 others => 1294 Has_Element (Container, First'Result) 1295 and P.Get (Positions (Container), First'Result) = 1); 1296 1297 function First_Element (Container : Set) return Element_Type with 1298 Global => null, 1299 Pre => not Is_Empty (Container), 1300 Post => 1301 First_Element'Result = E.Get (Elements (Container), 1) 1302 and E_Smaller_Than_Range 1303 (Elements (Container), 1304 2, 1305 Length (Container), 1306 First_Element'Result); 1307 1308 function Last (Container : Set) return Cursor with 1309 Global => null, 1310 Contract_Cases => 1311 (Length (Container) = 0 => 1312 Last'Result = No_Element, 1313 1314 others => 1315 Has_Element (Container, Last'Result) 1316 and P.Get (Positions (Container), Last'Result) = 1317 Length (Container)); 1318 1319 function Last_Element (Container : Set) return Element_Type with 1320 Global => null, 1321 Pre => not Is_Empty (Container), 1322 Post => 1323 Last_Element'Result = E.Get (Elements (Container), Length (Container)) 1324 and E_Bigger_Than_Range 1325 (Elements (Container), 1326 1, 1327 Length (Container) - 1, 1328 Last_Element'Result); 1329 1330 function Next (Container : Set; Position : Cursor) return Cursor with 1331 Global => null, 1332 Pre => 1333 Has_Element (Container, Position) or else Position = No_Element, 1334 Contract_Cases => 1335 (Position = No_Element 1336 or else P.Get (Positions (Container), Position) = Length (Container) 1337 => 1338 Next'Result = No_Element, 1339 1340 others => 1341 Has_Element (Container, Next'Result) 1342 and then P.Get (Positions (Container), Next'Result) = 1343 P.Get (Positions (Container), Position) + 1); 1344 1345 procedure Next (Container : Set; Position : in out Cursor) with 1346 Global => null, 1347 Pre => 1348 Has_Element (Container, Position) or else Position = No_Element, 1349 Contract_Cases => 1350 (Position = No_Element 1351 or else P.Get (Positions (Container), Position) = Length (Container) 1352 => 1353 Position = No_Element, 1354 1355 others => 1356 Has_Element (Container, Position) 1357 and then P.Get (Positions (Container), Position) = 1358 P.Get (Positions (Container), Position'Old) + 1); 1359 1360 function Previous (Container : Set; Position : Cursor) return Cursor with 1361 Global => null, 1362 Pre => 1363 Has_Element (Container, Position) or else Position = No_Element, 1364 Contract_Cases => 1365 (Position = No_Element 1366 or else P.Get (Positions (Container), Position) = 1 1367 => 1368 Previous'Result = No_Element, 1369 1370 others => 1371 Has_Element (Container, Previous'Result) 1372 and then P.Get (Positions (Container), Previous'Result) = 1373 P.Get (Positions (Container), Position) - 1); 1374 1375 procedure Previous (Container : Set; Position : in out Cursor) with 1376 Global => null, 1377 Pre => 1378 Has_Element (Container, Position) or else Position = No_Element, 1379 Contract_Cases => 1380 (Position = No_Element 1381 or else P.Get (Positions (Container), Position) = 1 1382 => 1383 Position = No_Element, 1384 1385 others => 1386 Has_Element (Container, Position) 1387 and then P.Get (Positions (Container), Position) = 1388 P.Get (Positions (Container), Position'Old) - 1); 1389 1390 function Find (Container : Set; Item : Element_Type) return Cursor with 1391 Global => null, 1392 Contract_Cases => 1393 1394 -- If Item is not contained in Container, Find returns No_Element 1395 1396 (not Contains (Model (Container), Item) => 1397 not P.Has_Key (Positions (Container), Find'Result) 1398 and Find'Result = No_Element, 1399 1400 -- Otherwise, Find returns a valid cursor in Container 1401 1402 others => 1403 P.Has_Key (Positions (Container), Find'Result) 1404 and P.Get (Positions (Container), Find'Result) = 1405 Find (Elements (Container), Item) 1406 1407 -- The element designated by the result of Find is Item 1408 1409 and Equivalent_Elements 1410 (Element (Container, Find'Result), Item)); 1411 1412 function Floor (Container : Set; Item : Element_Type) return Cursor with 1413 Global => null, 1414 Contract_Cases => 1415 (Length (Container) = 0 or else Item < First_Element (Container) => 1416 Floor'Result = No_Element, 1417 others => 1418 Has_Element (Container, Floor'Result) 1419 and 1420 not (Item < E.Get (Elements (Container), 1421 P.Get (Positions (Container), Floor'Result))) 1422 and E_Is_Find 1423 (Elements (Container), 1424 Item, 1425 P.Get (Positions (Container), Floor'Result))); 1426 1427 function Ceiling (Container : Set; Item : Element_Type) return Cursor with 1428 Global => null, 1429 Contract_Cases => 1430 (Length (Container) = 0 or else Last_Element (Container) < Item => 1431 Ceiling'Result = No_Element, 1432 others => 1433 Has_Element (Container, Ceiling'Result) 1434 and 1435 not (E.Get (Elements (Container), 1436 P.Get (Positions (Container), Ceiling'Result)) < 1437 Item) 1438 and E_Is_Find 1439 (Elements (Container), 1440 Item, 1441 P.Get (Positions (Container), Ceiling'Result))); 1442 1443 function Contains (Container : Set; Item : Element_Type) return Boolean with 1444 Global => null, 1445 Post => Contains'Result = Contains (Model (Container), Item); 1446 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 1447 1448 function Has_Element (Container : Set; Position : Cursor) return Boolean 1449 with 1450 Global => null, 1451 Post => 1452 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1453 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1454 1455 generic 1456 type Key_Type (<>) is private; 1457 1458 with function Key (Element : Element_Type) return Key_Type; 1459 1460 with function "<" (Left, Right : Key_Type) return Boolean is <>; 1461 1462 package Generic_Keys with SPARK_Mode is 1463 1464 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with 1465 Global => null, 1466 Post => 1467 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left)); 1468 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys); 1469 1470 package Formal_Model with Ghost is 1471 function E_Bigger_Than_Range 1472 (Container : E.Sequence; 1473 Fst : Positive_Count_Type; 1474 Lst : Count_Type; 1475 Key : Key_Type) return Boolean 1476 with 1477 Global => null, 1478 Pre => Lst <= E.Length (Container), 1479 Post => 1480 E_Bigger_Than_Range'Result = 1481 (for all I in Fst .. Lst => 1482 Generic_Keys.Key (E.Get (Container, I)) < Key); 1483 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range); 1484 1485 function E_Smaller_Than_Range 1486 (Container : E.Sequence; 1487 Fst : Positive_Count_Type; 1488 Lst : Count_Type; 1489 Key : Key_Type) return Boolean 1490 with 1491 Global => null, 1492 Pre => Lst <= E.Length (Container), 1493 Post => 1494 E_Smaller_Than_Range'Result = 1495 (for all I in Fst .. Lst => 1496 Key < Generic_Keys.Key (E.Get (Container, I))); 1497 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range); 1498 1499 function E_Is_Find 1500 (Container : E.Sequence; 1501 Key : Key_Type; 1502 Position : Count_Type) return Boolean 1503 with 1504 Global => null, 1505 Pre => Position - 1 <= E.Length (Container), 1506 Post => 1507 E_Is_Find'Result = 1508 1509 ((if Position > 0 then 1510 E_Bigger_Than_Range (Container, 1, Position - 1, Key)) 1511 1512 and (if Position < E.Length (Container) then 1513 E_Smaller_Than_Range 1514 (Container, 1515 Position + 1, 1516 E.Length (Container), 1517 Key))); 1518 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find); 1519 1520 function Find 1521 (Container : E.Sequence; 1522 Key : Key_Type) return Count_Type 1523 -- Search for Key in Container 1524 1525 with 1526 Global => null, 1527 Post => 1528 (if Find'Result > 0 then 1529 Find'Result <= E.Length (Container) 1530 and Equivalent_Keys 1531 (Key, Generic_Keys.Key (E.Get (Container, Find'Result))) 1532 and E_Is_Find (Container, Key, Find'Result)); 1533 1534 function M_Included_Except 1535 (Left : M.Set; 1536 Right : M.Set; 1537 Key : Key_Type) return Boolean 1538 with 1539 Global => null, 1540 Post => 1541 M_Included_Except'Result = 1542 (for all E of Left => 1543 Contains (Right, E) 1544 or Equivalent_Keys (Generic_Keys.Key (E), Key)); 1545 end Formal_Model; 1546 use Formal_Model; 1547 1548 function Key (Container : Set; Position : Cursor) return Key_Type with 1549 Global => null, 1550 Post => Key'Result = Key (Element (Container, Position)); 1551 pragma Annotate (GNATprove, Inline_For_Proof, Key); 1552 1553 function Element (Container : Set; Key : Key_Type) return Element_Type 1554 with 1555 Global => null, 1556 Pre => Contains (Container, Key), 1557 Post => 1558 Element'Result = Element (Container, Find (Container, Key)); 1559 pragma Annotate (GNATprove, Inline_For_Proof, Element); 1560 1561 procedure Replace 1562 (Container : in out Set; 1563 Key : Key_Type; 1564 New_Item : Element_Type) 1565 with 1566 Global => null, 1567 Pre => Contains (Container, Key), 1568 Post => 1569 Length (Container) = Length (Container)'Old 1570 1571 -- Key now maps to New_Item 1572 1573 and Element (Container, Key) = New_Item 1574 1575 -- New_Item is contained in Container 1576 1577 and Contains (Model (Container), New_Item) 1578 1579 -- Other elements are preserved 1580 1581 and M_Included_Except 1582 (Model (Container)'Old, 1583 Model (Container), 1584 Key) 1585 and M.Included_Except 1586 (Model (Container), 1587 Model (Container)'Old, 1588 New_Item) 1589 1590 -- Mapping from cursors to elements is preserved 1591 1592 and Mapping_Preserved_Except 1593 (E_Left => Elements (Container)'Old, 1594 E_Right => Elements (Container), 1595 P_Left => Positions (Container)'Old, 1596 P_Right => Positions (Container), 1597 Position => Find (Container, Key)) 1598 and Positions (Container) = Positions (Container)'Old; 1599 1600 procedure Exclude (Container : in out Set; Key : Key_Type) with 1601 Global => null, 1602 Post => not Contains (Container, Key), 1603 Contract_Cases => 1604 1605 -- If Key is not in Container, nothing is changed 1606 1607 (not Contains (Container, Key) => 1608 Model (Container) = Model (Container)'Old 1609 and Elements (Container) = Elements (Container)'Old 1610 and Positions (Container) = Positions (Container)'Old, 1611 1612 -- Otherwise, Key is removed from Container 1613 1614 others => 1615 Length (Container) = Length (Container)'Old - 1 1616 1617 -- Other elements are preserved 1618 1619 and Model (Container) <= Model (Container)'Old 1620 and M_Included_Except 1621 (Model (Container)'Old, 1622 Model (Container), 1623 Key) 1624 1625 -- The elements of Container located before Key are preserved 1626 1627 and E.Range_Equal 1628 (Left => Elements (Container)'Old, 1629 Right => Elements (Container), 1630 Fst => 1, 1631 Lst => Find (Elements (Container), Key)'Old - 1) 1632 1633 -- The elements located after Key are shifted by 1 1634 1635 and E.Range_Shifted 1636 (Left => Elements (Container), 1637 Right => Elements (Container)'Old, 1638 Fst => Find (Elements (Container), Key)'Old, 1639 Lst => Length (Container), 1640 Offset => 1) 1641 1642 -- A cursor has been removed from Container 1643 1644 and P_Positions_Shifted 1645 (Positions (Container), 1646 Positions (Container)'Old, 1647 Cut => Find (Elements (Container), Key)'Old)); 1648 1649 procedure Delete (Container : in out Set; Key : Key_Type) with 1650 Global => null, 1651 Pre => Contains (Container, Key), 1652 Post => 1653 Length (Container) = Length (Container)'Old - 1 1654 1655 -- Key is no longer in Container 1656 1657 and not Contains (Container, Key) 1658 1659 -- Other elements are preserved 1660 1661 and Model (Container) <= Model (Container)'Old 1662 and M_Included_Except 1663 (Model (Container)'Old, 1664 Model (Container), 1665 Key) 1666 1667 -- The elements of Container located before Key are preserved 1668 1669 and E.Range_Equal 1670 (Left => Elements (Container)'Old, 1671 Right => Elements (Container), 1672 Fst => 1, 1673 Lst => Find (Elements (Container), Key)'Old - 1) 1674 1675 -- The elements located after Key are shifted by 1 1676 1677 and E.Range_Shifted 1678 (Left => Elements (Container), 1679 Right => Elements (Container)'Old, 1680 Fst => Find (Elements (Container), Key)'Old, 1681 Lst => Length (Container), 1682 Offset => 1) 1683 1684 -- A cursor has been removed from Container 1685 1686 and P_Positions_Shifted 1687 (Positions (Container), 1688 Positions (Container)'Old, 1689 Cut => Find (Elements (Container), Key)'Old); 1690 1691 function Find (Container : Set; Key : Key_Type) return Cursor with 1692 Global => null, 1693 Contract_Cases => 1694 1695 -- If Key is not contained in Container, Find returns No_Element 1696 1697 ((for all E of Model (Container) => 1698 not Equivalent_Keys (Key, Generic_Keys.Key (E))) => 1699 not P.Has_Key (Positions (Container), Find'Result) 1700 and Find'Result = No_Element, 1701 1702 -- Otherwise, Find returns a valid cursor in Container 1703 1704 others => 1705 P.Has_Key (Positions (Container), Find'Result) 1706 and P.Get (Positions (Container), Find'Result) = 1707 Find (Elements (Container), Key) 1708 1709 -- The element designated by the result of Find is Key 1710 1711 and Equivalent_Keys 1712 (Generic_Keys.Key (Element (Container, Find'Result)), Key)); 1713 1714 function Floor (Container : Set; Key : Key_Type) return Cursor with 1715 Global => null, 1716 Contract_Cases => 1717 (Length (Container) = 0 1718 or else Key < Generic_Keys.Key (First_Element (Container)) => 1719 Floor'Result = No_Element, 1720 others => 1721 Has_Element (Container, Floor'Result) 1722 and 1723 not (Key < 1724 Generic_Keys.Key 1725 (E.Get (Elements (Container), 1726 P.Get (Positions (Container), Floor'Result)))) 1727 and E_Is_Find 1728 (Elements (Container), 1729 Key, 1730 P.Get (Positions (Container), Floor'Result))); 1731 1732 function Ceiling (Container : Set; Key : Key_Type) return Cursor with 1733 Global => null, 1734 Contract_Cases => 1735 (Length (Container) = 0 1736 or else Generic_Keys.Key (Last_Element (Container)) < Key => 1737 Ceiling'Result = No_Element, 1738 others => 1739 Has_Element (Container, Ceiling'Result) 1740 and 1741 not (Generic_Keys.Key 1742 (E.Get (Elements (Container), 1743 P.Get (Positions (Container), Ceiling'Result))) 1744 < Key) 1745 and E_Is_Find 1746 (Elements (Container), 1747 Key, 1748 P.Get (Positions (Container), Ceiling'Result))); 1749 1750 function Contains (Container : Set; Key : Key_Type) return Boolean with 1751 Global => null, 1752 Post => 1753 Contains'Result = 1754 (for some E of Model (Container) => 1755 Equivalent_Keys (Key, Generic_Keys.Key (E))); 1756 1757 end Generic_Keys; 1758 1759private 1760 pragma SPARK_Mode (Off); 1761 1762 pragma Inline (Next); 1763 pragma Inline (Previous); 1764 1765 type Node_Type is record 1766 Has_Element : Boolean := False; 1767 Parent : Count_Type := 0; 1768 Left : Count_Type := 0; 1769 Right : Count_Type := 0; 1770 Color : Red_Black_Trees.Color_Type; 1771 Element : Element_Type; 1772 end record; 1773 1774 package Tree_Types is 1775 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); 1776 1777 type Set (Capacity : Count_Type) is 1778 new Tree_Types.Tree_Type (Capacity) with null record; 1779 1780 use Red_Black_Trees; 1781 1782 Empty_Set : constant Set := (Capacity => 0, others => <>); 1783 1784end Ada.Containers.Formal_Ordered_Sets; 1785