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 _ M A P S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2019, Free Software Foundation, Inc. -- 10-- -- 11-- This specification is derived from the Ada Reference Manual for use with -- 12-- GNAT. The copyright notice above, and the license provisions that follow -- 13-- apply solely to the contents of the part following the private keyword. -- 14-- -- 15-- GNAT is free software; you can redistribute it and/or modify it under -- 16-- terms of the GNU General Public License as published by the Free Soft- -- 17-- ware Foundation; either version 3, or (at your option) any later ver- -- 18-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 19-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 20-- or FITNESS FOR A PARTICULAR PURPOSE. -- 21-- -- 22-- As a special exception under Section 7 of GPL version 3, you are granted -- 23-- additional permissions described in the GCC Runtime Library Exception, -- 24-- version 3.1, as published by the Free Software Foundation. -- 25-- -- 26-- You should have received a copy of the GNU General Public License and -- 27-- a copy of the GCC Runtime Library Exception along with this program; -- 28-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 29-- <http://www.gnu.org/licenses/>. -- 30------------------------------------------------------------------------------ 31 32-- This spec is derived from package Ada.Containers.Bounded_Ordered_Maps 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 a 44-- container C and its previous version C'Old) for expressing properties, 45-- which is not possible if cursors encapsulate an access to the underlying 46-- container. The operators "<" and ">" that could not be modified that way 47-- have been removed. 48 49-- Iteration over maps is done using the Iterable aspect, which is SPARK 50-- compatible. "For of" iteration ranges over keys instead of elements. 51 52with Ada.Containers.Functional_Vectors; 53with Ada.Containers.Functional_Maps; 54private with Ada.Containers.Red_Black_Trees; 55 56generic 57 type Key_Type is private; 58 type Element_Type is private; 59 60 with function "<" (Left, Right : Key_Type) return Boolean is <>; 61 with function "=" (Left, Right : Element_Type) return Boolean is <>; 62 63package Ada.Containers.Formal_Ordered_Maps with 64 SPARK_Mode 65is 66 pragma Annotate (CodePeer, Skip_Analysis); 67 68 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with 69 Global => null, 70 Post => 71 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left)); 72 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys); 73 74 type Map (Capacity : Count_Type) is private with 75 Iterable => (First => First, 76 Next => Next, 77 Has_Element => Has_Element, 78 Element => Key), 79 Default_Initial_Condition => Is_Empty (Map); 80 pragma Preelaborable_Initialization (Map); 81 82 type Cursor is record 83 Node : Count_Type; 84 end record; 85 86 No_Element : constant Cursor := (Node => 0); 87 88 Empty_Map : constant Map; 89 90 function Length (Container : Map) return Count_Type with 91 Global => null, 92 Post => Length'Result <= Container.Capacity; 93 94 pragma Unevaluated_Use_Of_Old (Allow); 95 96 package Formal_Model with Ghost is 97 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; 98 99 package M is new Ada.Containers.Functional_Maps 100 (Element_Type => Element_Type, 101 Key_Type => Key_Type, 102 Equivalent_Keys => Equivalent_Keys); 103 104 function "=" 105 (Left : M.Map; 106 Right : M.Map) return Boolean renames M."="; 107 108 function "<=" 109 (Left : M.Map; 110 Right : M.Map) return Boolean renames M."<="; 111 112 package K is new Ada.Containers.Functional_Vectors 113 (Element_Type => Key_Type, 114 Index_Type => Positive_Count_Type); 115 116 function "=" 117 (Left : K.Sequence; 118 Right : K.Sequence) return Boolean renames K."="; 119 120 function "<" 121 (Left : K.Sequence; 122 Right : K.Sequence) return Boolean renames K."<"; 123 124 function "<=" 125 (Left : K.Sequence; 126 Right : K.Sequence) return Boolean renames K."<="; 127 128 function K_Bigger_Than_Range 129 (Container : K.Sequence; 130 Fst : Positive_Count_Type; 131 Lst : Count_Type; 132 Key : Key_Type) return Boolean 133 with 134 Global => null, 135 Pre => Lst <= K.Length (Container), 136 Post => 137 K_Bigger_Than_Range'Result = 138 (for all I in Fst .. Lst => K.Get (Container, I) < Key); 139 pragma Annotate (GNATprove, Inline_For_Proof, K_Bigger_Than_Range); 140 141 function K_Smaller_Than_Range 142 (Container : K.Sequence; 143 Fst : Positive_Count_Type; 144 Lst : Count_Type; 145 Key : Key_Type) return Boolean 146 with 147 Global => null, 148 Pre => Lst <= K.Length (Container), 149 Post => 150 K_Smaller_Than_Range'Result = 151 (for all I in Fst .. Lst => Key < K.Get (Container, I)); 152 pragma Annotate (GNATprove, Inline_For_Proof, K_Smaller_Than_Range); 153 154 function K_Is_Find 155 (Container : K.Sequence; 156 Key : Key_Type; 157 Position : Count_Type) return Boolean 158 with 159 Global => null, 160 Pre => Position - 1 <= K.Length (Container), 161 Post => 162 K_Is_Find'Result = 163 ((if Position > 0 then 164 K_Bigger_Than_Range (Container, 1, Position - 1, Key)) 165 166 and 167 (if Position < K.Length (Container) then 168 K_Smaller_Than_Range 169 (Container, 170 Position + 1, 171 K.Length (Container), 172 Key))); 173 pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find); 174 175 function Find (Container : K.Sequence; Key : Key_Type) return Count_Type 176 -- Search for Key in Container 177 178 with 179 Global => null, 180 Post => 181 (if Find'Result > 0 then 182 Find'Result <= K.Length (Container) 183 and Equivalent_Keys (Key, K.Get (Container, Find'Result))); 184 185 package P is new Ada.Containers.Functional_Maps 186 (Key_Type => Cursor, 187 Element_Type => Positive_Count_Type, 188 Equivalent_Keys => "=", 189 Enable_Handling_Of_Equivalence => False); 190 191 function "=" 192 (Left : P.Map; 193 Right : P.Map) return Boolean renames P."="; 194 195 function "<=" 196 (Left : P.Map; 197 Right : P.Map) return Boolean renames P."<="; 198 199 function P_Positions_Shifted 200 (Small : P.Map; 201 Big : P.Map; 202 Cut : Positive_Count_Type; 203 Count : Count_Type := 1) return Boolean 204 with 205 Global => null, 206 Post => 207 P_Positions_Shifted'Result = 208 209 -- Big contains all cursors of Small 210 211 (P.Keys_Included (Small, Big) 212 213 -- Cursors located before Cut are not moved, cursors located 214 -- after are shifted by Count. 215 216 and (for all I of Small => 217 (if P.Get (Small, I) < Cut then 218 P.Get (Big, I) = P.Get (Small, I) 219 else 220 P.Get (Big, I) - Count = P.Get (Small, I))) 221 222 -- New cursors of Big (if any) are between Cut and Cut - 1 + 223 -- Count. 224 225 and (for all I of Big => 226 P.Has_Key (Small, I) 227 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); 228 229 function Model (Container : Map) return M.Map with 230 -- The high-level model of a map is a map from keys to elements. Neither 231 -- cursors nor order of elements are represented in this model. Keys are 232 -- modeled up to equivalence. 233 234 Ghost, 235 Global => null; 236 237 function Keys (Container : Map) return K.Sequence with 238 -- The Keys sequence represents the underlying list structure of maps 239 -- that is used for iteration. It stores the actual values of keys in 240 -- the map. It does not model cursors nor elements. 241 242 Ghost, 243 Global => null, 244 Post => 245 K.Length (Keys'Result) = Length (Container) 246 247 -- It only contains keys contained in Model 248 249 and (for all Key of Keys'Result => 250 M.Has_Key (Model (Container), Key)) 251 252 -- It contains all the keys contained in Model 253 254 and (for all Key of Model (Container) => 255 (Find (Keys'Result, Key) > 0 256 and then Equivalent_Keys 257 (K.Get (Keys'Result, Find (Keys'Result, Key)), 258 Key))) 259 260 -- It is sorted in increasing order 261 262 and (for all I in 1 .. Length (Container) => 263 Find (Keys'Result, K.Get (Keys'Result, I)) = I 264 and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I)); 265 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); 266 267 function Positions (Container : Map) return P.Map with 268 -- The Positions map is used to model cursors. It only contains valid 269 -- cursors and maps them to their position in the container. 270 271 Ghost, 272 Global => null, 273 Post => 274 not P.Has_Key (Positions'Result, No_Element) 275 276 -- Positions of cursors are smaller than the container's length. 277 278 and then 279 (for all I of Positions'Result => 280 P.Get (Positions'Result, I) in 1 .. Length (Container) 281 282 -- No two cursors have the same position. Note that we do not 283 -- state that there is a cursor in the map for each position, as 284 -- it is rarely needed. 285 286 and then 287 (for all J of Positions'Result => 288 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) 289 then I = J))); 290 291 procedure Lift_Abstraction_Level (Container : Map) with 292 -- Lift_Abstraction_Level is a ghost procedure that does nothing but 293 -- assume that we can access the same elements by iterating over 294 -- positions or cursors. 295 -- This information is not generally useful except when switching from 296 -- a low-level, cursor-aware view of a container, to a high-level, 297 -- position-based view. 298 299 Ghost, 300 Global => null, 301 Post => 302 (for all Key of Keys (Container) => 303 (for some I of Positions (Container) => 304 K.Get (Keys (Container), P.Get (Positions (Container), I)) = 305 Key)); 306 307 function Contains 308 (C : M.Map; 309 K : Key_Type) return Boolean renames M.Has_Key; 310 -- To improve readability of contracts, we rename the function used to 311 -- search for a key in the model to Contains. 312 313 function Element 314 (C : M.Map; 315 K : Key_Type) return Element_Type renames M.Get; 316 -- To improve readability of contracts, we rename the function used to 317 -- access an element in the model to Element. 318 end Formal_Model; 319 use Formal_Model; 320 321 function "=" (Left, Right : Map) return Boolean with 322 Global => null, 323 Post => "="'Result = (Model (Left) = Model (Right)); 324 325 function Is_Empty (Container : Map) return Boolean with 326 Global => null, 327 Post => Is_Empty'Result = (Length (Container) = 0); 328 329 procedure Clear (Container : in out Map) with 330 Global => null, 331 Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); 332 333 procedure Assign (Target : in out Map; Source : Map) with 334 Global => null, 335 Pre => Target.Capacity >= Length (Source), 336 Post => 337 Model (Target) = Model (Source) 338 and Keys (Target) = Keys (Source) 339 and Length (Source) = Length (Target); 340 341 function Copy (Source : Map; Capacity : Count_Type := 0) return Map with 342 Global => null, 343 Pre => Capacity = 0 or else Capacity >= Source.Capacity, 344 Post => 345 Model (Copy'Result) = Model (Source) 346 and Keys (Copy'Result) = Keys (Source) 347 and Positions (Copy'Result) = Positions (Source) 348 and (if Capacity = 0 then 349 Copy'Result.Capacity = Source.Capacity 350 else 351 Copy'Result.Capacity = Capacity); 352 353 function Key (Container : Map; Position : Cursor) return Key_Type with 354 Global => null, 355 Pre => Has_Element (Container, Position), 356 Post => 357 Key'Result = 358 K.Get (Keys (Container), P.Get (Positions (Container), Position)); 359 pragma Annotate (GNATprove, Inline_For_Proof, Key); 360 361 function Element 362 (Container : Map; 363 Position : Cursor) return Element_Type 364 with 365 Global => null, 366 Pre => Has_Element (Container, Position), 367 Post => 368 Element'Result = Element (Model (Container), Key (Container, Position)); 369 pragma Annotate (GNATprove, Inline_For_Proof, Element); 370 371 procedure Replace_Element 372 (Container : in out Map; 373 Position : Cursor; 374 New_Item : Element_Type) 375 with 376 Global => null, 377 Pre => Has_Element (Container, Position), 378 Post => 379 380 -- Order of keys and cursors is preserved 381 382 Keys (Container) = Keys (Container)'Old 383 and Positions (Container) = Positions (Container)'Old 384 385 -- New_Item is now associated with the key at position Position in 386 -- Container. 387 388 and Element (Container, Position) = New_Item 389 390 -- Elements associated with other keys are preserved 391 392 and M.Same_Keys (Model (Container), Model (Container)'Old) 393 and M.Elements_Equal_Except 394 (Model (Container), 395 Model (Container)'Old, 396 Key (Container, Position)); 397 398 procedure Move (Target : in out Map; Source : in out Map) with 399 Global => null, 400 Pre => Target.Capacity >= Length (Source), 401 Post => 402 Model (Target) = Model (Source)'Old 403 and Keys (Target) = Keys (Source)'Old 404 and Length (Source)'Old = Length (Target) 405 and Length (Source) = 0; 406 407 procedure Insert 408 (Container : in out Map; 409 Key : Key_Type; 410 New_Item : Element_Type; 411 Position : out Cursor; 412 Inserted : out Boolean) 413 with 414 Global => null, 415 Pre => 416 Length (Container) < Container.Capacity or Contains (Container, Key), 417 Post => 418 Contains (Container, Key) 419 and Has_Element (Container, Position) 420 and Equivalent_Keys 421 (Formal_Ordered_Maps.Key (Container, Position), Key) 422 and K_Is_Find 423 (Keys (Container), 424 Key, 425 P.Get (Positions (Container), Position)), 426 Contract_Cases => 427 428 -- If Key is already in Container, it is not modified and Inserted is 429 -- set to False. 430 431 (Contains (Container, Key) => 432 not Inserted 433 and Model (Container) = Model (Container)'Old 434 and Keys (Container) = Keys (Container)'Old 435 and Positions (Container) = Positions (Container)'Old, 436 437 -- Otherwise, Key is inserted in Container and Inserted is set to True 438 439 others => 440 Inserted 441 and Length (Container) = Length (Container)'Old + 1 442 443 -- Key now maps to New_Item 444 445 and Formal_Ordered_Maps.Key (Container, Position) = Key 446 and Element (Model (Container), Key) = New_Item 447 448 -- Other mappings are preserved 449 450 and Model (Container)'Old <= Model (Container) 451 and M.Keys_Included_Except 452 (Model (Container), 453 Model (Container)'Old, 454 Key) 455 456 -- The keys of Container located before Position are preserved 457 458 and K.Range_Equal 459 (Left => Keys (Container)'Old, 460 Right => Keys (Container), 461 Fst => 1, 462 Lst => P.Get (Positions (Container), Position) - 1) 463 464 -- Other keys are shifted by 1 465 466 and K.Range_Shifted 467 (Left => Keys (Container)'Old, 468 Right => Keys (Container), 469 Fst => P.Get (Positions (Container), Position), 470 Lst => Length (Container)'Old, 471 Offset => 1) 472 473 -- A new cursor has been inserted at position Position in 474 -- Container. 475 476 and P_Positions_Shifted 477 (Positions (Container)'Old, 478 Positions (Container), 479 Cut => P.Get (Positions (Container), Position))); 480 481 procedure Insert 482 (Container : in out Map; 483 Key : Key_Type; 484 New_Item : Element_Type) 485 with 486 Global => null, 487 Pre => 488 Length (Container) < Container.Capacity 489 and then (not Contains (Container, Key)), 490 Post => 491 Length (Container) = Length (Container)'Old + 1 492 and Contains (Container, Key) 493 494 -- Key now maps to New_Item 495 496 and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key 497 and Element (Model (Container), Key) = New_Item 498 499 -- Other mappings are preserved 500 501 and Model (Container)'Old <= Model (Container) 502 and M.Keys_Included_Except 503 (Model (Container), 504 Model (Container)'Old, 505 Key) 506 507 -- The keys of Container located before Key are preserved 508 509 and K.Range_Equal 510 (Left => Keys (Container)'Old, 511 Right => Keys (Container), 512 Fst => 1, 513 Lst => Find (Keys (Container), Key) - 1) 514 515 -- Other keys are shifted by 1 516 517 and K.Range_Shifted 518 (Left => Keys (Container)'Old, 519 Right => Keys (Container), 520 Fst => Find (Keys (Container), Key), 521 Lst => Length (Container)'Old, 522 Offset => 1) 523 524 -- A new cursor has been inserted in Container 525 526 and P_Positions_Shifted 527 (Positions (Container)'Old, 528 Positions (Container), 529 Cut => Find (Keys (Container), Key)); 530 531 procedure Include 532 (Container : in out Map; 533 Key : Key_Type; 534 New_Item : Element_Type) 535 with 536 Global => null, 537 Pre => 538 Length (Container) < Container.Capacity or Contains (Container, Key), 539 Post => 540 Contains (Container, Key) and Element (Container, Key) = New_Item, 541 Contract_Cases => 542 543 -- If Key is already in Container, Key is mapped to New_Item 544 545 (Contains (Container, Key) => 546 547 -- Cursors are preserved 548 549 Positions (Container) = Positions (Container)'Old 550 551 -- The key equivalent to Key in Container is replaced by Key 552 553 and K.Get 554 (Keys (Container), Find (Keys (Container), Key)) = Key 555 556 and K.Equal_Except 557 (Keys (Container)'Old, 558 Keys (Container), 559 Find (Keys (Container), Key)) 560 561 -- Elements associated with other keys are preserved 562 563 and M.Same_Keys (Model (Container), Model (Container)'Old) 564 and M.Elements_Equal_Except 565 (Model (Container), 566 Model (Container)'Old, 567 Key), 568 569 -- Otherwise, Key is inserted in Container 570 571 others => 572 Length (Container) = Length (Container)'Old + 1 573 574 -- Other mappings are preserved 575 576 and Model (Container)'Old <= Model (Container) 577 and M.Keys_Included_Except 578 (Model (Container), 579 Model (Container)'Old, 580 Key) 581 582 -- Key is inserted in Container 583 584 and K.Get 585 (Keys (Container), Find (Keys (Container), Key)) = Key 586 587 -- The keys of Container located before Key are preserved 588 589 and K.Range_Equal 590 (Left => Keys (Container)'Old, 591 Right => Keys (Container), 592 Fst => 1, 593 Lst => Find (Keys (Container), Key) - 1) 594 595 -- Other keys are shifted by 1 596 597 and K.Range_Shifted 598 (Left => Keys (Container)'Old, 599 Right => Keys (Container), 600 Fst => Find (Keys (Container), Key), 601 Lst => Length (Container)'Old, 602 Offset => 1) 603 604 -- A new cursor has been inserted in Container 605 606 and P_Positions_Shifted 607 (Positions (Container)'Old, 608 Positions (Container), 609 Cut => Find (Keys (Container), Key))); 610 611 procedure Replace 612 (Container : in out Map; 613 Key : Key_Type; 614 New_Item : Element_Type) 615 with 616 Global => null, 617 Pre => Contains (Container, Key), 618 Post => 619 620 -- Cursors are preserved 621 622 Positions (Container) = Positions (Container)'Old 623 624 -- The key equivalent to Key in Container is replaced by Key 625 626 and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key 627 and K.Equal_Except 628 (Keys (Container)'Old, 629 Keys (Container), 630 Find (Keys (Container), Key)) 631 632 -- New_Item is now associated with the Key in Container 633 634 and Element (Model (Container), Key) = New_Item 635 636 -- Elements associated with other keys are preserved 637 638 and M.Same_Keys (Model (Container), Model (Container)'Old) 639 and M.Elements_Equal_Except 640 (Model (Container), 641 Model (Container)'Old, 642 Key); 643 644 procedure Exclude (Container : in out Map; Key : Key_Type) with 645 Global => null, 646 Post => not Contains (Container, Key), 647 Contract_Cases => 648 649 -- If Key is not in Container, nothing is changed 650 651 (not Contains (Container, Key) => 652 Model (Container) = Model (Container)'Old 653 and Keys (Container) = Keys (Container)'Old 654 and Positions (Container) = Positions (Container)'Old, 655 656 -- Otherwise, Key is removed from Container 657 658 others => 659 Length (Container) = Length (Container)'Old - 1 660 661 -- Other mappings are preserved 662 663 and Model (Container) <= Model (Container)'Old 664 and M.Keys_Included_Except 665 (Model (Container)'Old, 666 Model (Container), 667 Key) 668 669 -- The keys of Container located before Key are preserved 670 671 and K.Range_Equal 672 (Left => Keys (Container)'Old, 673 Right => Keys (Container), 674 Fst => 1, 675 Lst => Find (Keys (Container), Key)'Old - 1) 676 677 -- The keys located after Key are shifted by 1 678 679 and K.Range_Shifted 680 (Left => Keys (Container), 681 Right => Keys (Container)'Old, 682 Fst => Find (Keys (Container), Key)'Old, 683 Lst => Length (Container), 684 Offset => 1) 685 686 -- A cursor has been removed from Container 687 688 and P_Positions_Shifted 689 (Positions (Container), 690 Positions (Container)'Old, 691 Cut => Find (Keys (Container), Key)'Old)); 692 693 procedure Delete (Container : in out Map; Key : Key_Type) with 694 Global => null, 695 Pre => Contains (Container, Key), 696 Post => 697 Length (Container) = Length (Container)'Old - 1 698 699 -- Key is no longer in Container 700 701 and not Contains (Container, Key) 702 703 -- Other mappings are preserved 704 705 and Model (Container) <= Model (Container)'Old 706 and M.Keys_Included_Except 707 (Model (Container)'Old, 708 Model (Container), 709 Key) 710 711 -- The keys of Container located before Key are preserved 712 713 and K.Range_Equal 714 (Left => Keys (Container)'Old, 715 Right => Keys (Container), 716 Fst => 1, 717 Lst => Find (Keys (Container), Key)'Old - 1) 718 719 -- The keys located after Key are shifted by 1 720 721 and K.Range_Shifted 722 (Left => Keys (Container), 723 Right => Keys (Container)'Old, 724 Fst => Find (Keys (Container), Key)'Old, 725 Lst => Length (Container), 726 Offset => 1) 727 728 -- A cursor has been removed from Container 729 730 and P_Positions_Shifted 731 (Positions (Container), 732 Positions (Container)'Old, 733 Cut => Find (Keys (Container), Key)'Old); 734 735 procedure Delete (Container : in out Map; Position : in out Cursor) with 736 Global => null, 737 Pre => Has_Element (Container, Position), 738 Post => 739 Position = No_Element 740 and Length (Container) = Length (Container)'Old - 1 741 742 -- The key at position Position is no longer in Container 743 744 and not Contains (Container, Key (Container, Position)'Old) 745 and not P.Has_Key (Positions (Container), Position'Old) 746 747 -- Other mappings are preserved 748 749 and Model (Container) <= Model (Container)'Old 750 and M.Keys_Included_Except 751 (Model (Container)'Old, 752 Model (Container), 753 Key (Container, Position)'Old) 754 755 -- The keys of Container located before Position are preserved. 756 757 and K.Range_Equal 758 (Left => Keys (Container)'Old, 759 Right => Keys (Container), 760 Fst => 1, 761 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) 762 763 -- The keys located after Position are shifted by 1 764 765 and K.Range_Shifted 766 (Left => Keys (Container), 767 Right => Keys (Container)'Old, 768 Fst => P.Get (Positions (Container)'Old, Position'Old), 769 Lst => Length (Container), 770 Offset => 1) 771 772 -- Position has been removed from Container 773 774 and P_Positions_Shifted 775 (Positions (Container), 776 Positions (Container)'Old, 777 Cut => P.Get (Positions (Container)'Old, Position'Old)); 778 779 procedure Delete_First (Container : in out Map) with 780 Global => null, 781 Contract_Cases => 782 (Length (Container) = 0 => Length (Container) = 0, 783 others => 784 Length (Container) = Length (Container)'Old - 1 785 786 -- The first key has been removed from Container 787 788 and not Contains (Container, First_Key (Container)'Old) 789 790 -- Other mappings are preserved 791 792 and Model (Container) <= Model (Container)'Old 793 and M.Keys_Included_Except 794 (Model (Container)'Old, 795 Model (Container), 796 First_Key (Container)'Old) 797 798 -- Other keys are shifted by 1 799 800 and K.Range_Shifted 801 (Left => Keys (Container), 802 Right => Keys (Container)'Old, 803 Fst => 1, 804 Lst => Length (Container), 805 Offset => 1) 806 807 -- First has been removed from Container 808 809 and P_Positions_Shifted 810 (Positions (Container), 811 Positions (Container)'Old, 812 Cut => 1)); 813 814 procedure Delete_Last (Container : in out Map) with 815 Global => null, 816 Contract_Cases => 817 (Length (Container) = 0 => Length (Container) = 0, 818 others => 819 Length (Container) = Length (Container)'Old - 1 820 821 -- The last key has been removed from Container 822 823 and not Contains (Container, Last_Key (Container)'Old) 824 825 -- Other mappings are preserved 826 827 and Model (Container) <= Model (Container)'Old 828 and M.Keys_Included_Except 829 (Model (Container)'Old, 830 Model (Container), 831 Last_Key (Container)'Old) 832 833 -- Others keys of Container are preserved 834 835 and K.Range_Equal 836 (Left => Keys (Container)'Old, 837 Right => Keys (Container), 838 Fst => 1, 839 Lst => Length (Container)) 840 841 -- Last cursor has been removed from Container 842 843 and Positions (Container) <= Positions (Container)'Old); 844 845 function First (Container : Map) return Cursor with 846 Global => null, 847 Contract_Cases => 848 (Length (Container) = 0 => 849 First'Result = No_Element, 850 851 others => 852 Has_Element (Container, First'Result) 853 and P.Get (Positions (Container), First'Result) = 1); 854 855 function First_Element (Container : Map) return Element_Type with 856 Global => null, 857 Pre => not Is_Empty (Container), 858 Post => 859 First_Element'Result = 860 Element (Model (Container), First_Key (Container)); 861 862 function First_Key (Container : Map) return Key_Type with 863 Global => null, 864 Pre => not Is_Empty (Container), 865 Post => 866 First_Key'Result = K.Get (Keys (Container), 1) 867 and K_Smaller_Than_Range 868 (Keys (Container), 2, Length (Container), First_Key'Result); 869 870 function Last (Container : Map) return Cursor with 871 Global => null, 872 Contract_Cases => 873 (Length (Container) = 0 => 874 Last'Result = No_Element, 875 876 others => 877 Has_Element (Container, Last'Result) 878 and P.Get (Positions (Container), Last'Result) = 879 Length (Container)); 880 881 function Last_Element (Container : Map) return Element_Type with 882 Global => null, 883 Pre => not Is_Empty (Container), 884 Post => 885 Last_Element'Result = Element (Model (Container), Last_Key (Container)); 886 887 function Last_Key (Container : Map) return Key_Type with 888 Global => null, 889 Pre => not Is_Empty (Container), 890 Post => 891 Last_Key'Result = K.Get (Keys (Container), Length (Container)) 892 and K_Bigger_Than_Range 893 (Keys (Container), 1, Length (Container) - 1, Last_Key'Result); 894 895 function Next (Container : Map; Position : Cursor) return Cursor with 896 Global => null, 897 Pre => 898 Has_Element (Container, Position) or else Position = No_Element, 899 Contract_Cases => 900 (Position = No_Element 901 or else P.Get (Positions (Container), Position) = Length (Container) 902 => 903 Next'Result = No_Element, 904 905 others => 906 Has_Element (Container, Next'Result) 907 and then P.Get (Positions (Container), Next'Result) = 908 P.Get (Positions (Container), Position) + 1); 909 910 procedure Next (Container : Map; Position : in out Cursor) with 911 Global => null, 912 Pre => 913 Has_Element (Container, Position) or else Position = No_Element, 914 Contract_Cases => 915 (Position = No_Element 916 or else P.Get (Positions (Container), Position) = Length (Container) 917 => 918 Position = No_Element, 919 920 others => 921 Has_Element (Container, Position) 922 and then P.Get (Positions (Container), Position) = 923 P.Get (Positions (Container), Position'Old) + 1); 924 925 function Previous (Container : Map; Position : Cursor) return Cursor with 926 Global => null, 927 Pre => 928 Has_Element (Container, Position) or else Position = No_Element, 929 Contract_Cases => 930 (Position = No_Element 931 or else P.Get (Positions (Container), Position) = 1 932 => 933 Previous'Result = No_Element, 934 935 others => 936 Has_Element (Container, Previous'Result) 937 and then P.Get (Positions (Container), Previous'Result) = 938 P.Get (Positions (Container), Position) - 1); 939 940 procedure Previous (Container : Map; Position : in out Cursor) with 941 Global => null, 942 Pre => 943 Has_Element (Container, Position) or else Position = No_Element, 944 Contract_Cases => 945 (Position = No_Element 946 or else P.Get (Positions (Container), Position) = 1 947 => 948 Position = No_Element, 949 950 others => 951 Has_Element (Container, Position) 952 and then P.Get (Positions (Container), Position) = 953 P.Get (Positions (Container), Position'Old) - 1); 954 955 function Find (Container : Map; Key : Key_Type) return Cursor with 956 Global => null, 957 Contract_Cases => 958 959 -- If Key is not contained in Container, Find returns No_Element 960 961 (not Contains (Model (Container), Key) => 962 not P.Has_Key (Positions (Container), Find'Result) 963 and Find'Result = No_Element, 964 965 -- Otherwise, Find returns a valid cursor in Container 966 967 others => 968 P.Has_Key (Positions (Container), Find'Result) 969 and P.Get (Positions (Container), Find'Result) = 970 Find (Keys (Container), Key) 971 972 -- The key designated by the result of Find is Key 973 974 and Equivalent_Keys 975 (Formal_Ordered_Maps.Key (Container, Find'Result), Key)); 976 977 function Element (Container : Map; Key : Key_Type) return Element_Type with 978 Global => null, 979 Pre => Contains (Container, Key), 980 Post => Element'Result = Element (Model (Container), Key); 981 pragma Annotate (GNATprove, Inline_For_Proof, Element); 982 983 function Floor (Container : Map; Key : Key_Type) return Cursor with 984 Global => null, 985 Contract_Cases => 986 (Length (Container) = 0 or else Key < First_Key (Container) => 987 Floor'Result = No_Element, 988 989 others => 990 Has_Element (Container, Floor'Result) 991 and not (Key < K.Get (Keys (Container), 992 P.Get (Positions (Container), Floor'Result))) 993 and K_Is_Find 994 (Keys (Container), 995 Key, 996 P.Get (Positions (Container), Floor'Result))); 997 998 function Ceiling (Container : Map; Key : Key_Type) return Cursor with 999 Global => null, 1000 Contract_Cases => 1001 (Length (Container) = 0 or else Last_Key (Container) < Key => 1002 Ceiling'Result = No_Element, 1003 others => 1004 Has_Element (Container, Ceiling'Result) 1005 and not (K.Get 1006 (Keys (Container), 1007 P.Get (Positions (Container), Ceiling'Result)) < Key) 1008 and K_Is_Find 1009 (Keys (Container), 1010 Key, 1011 P.Get (Positions (Container), Ceiling'Result))); 1012 1013 function Contains (Container : Map; Key : Key_Type) return Boolean with 1014 Global => null, 1015 Post => Contains'Result = Contains (Model (Container), Key); 1016 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 1017 1018 function Has_Element (Container : Map; Position : Cursor) return Boolean 1019 with 1020 Global => null, 1021 Post => 1022 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1023 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1024 1025private 1026 pragma SPARK_Mode (Off); 1027 1028 pragma Inline (Next); 1029 pragma Inline (Previous); 1030 1031 subtype Node_Access is Count_Type; 1032 1033 use Red_Black_Trees; 1034 1035 type Node_Type is record 1036 Has_Element : Boolean := False; 1037 Parent : Node_Access := 0; 1038 Left : Node_Access := 0; 1039 Right : Node_Access := 0; 1040 Color : Red_Black_Trees.Color_Type := Red; 1041 Key : Key_Type; 1042 Element : Element_Type; 1043 end record; 1044 1045 package Tree_Types is 1046 new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); 1047 1048 type Map (Capacity : Count_Type) is 1049 new Tree_Types.Tree_Type (Capacity) with null record; 1050 1051 Empty_Map : constant Map := (Capacity => 0, others => <>); 1052 1053end Ada.Containers.Formal_Ordered_Maps; 1054