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