gcc/ada/a-cforma.ads

   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-2017, 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
  52 with Ada.Containers.Functional_Vectors;
  53 with Ada.Containers.Functional_Maps;
  54 private with Ada.Containers.Red_Black_Trees;
  55
  56 generic
  57    type Key_Type is private;
  58    type Element_Type is private;
  59
  60    with function "<" (Left, Right : Key_Type) return Boolean is <>;
  61
  62 package Ada.Containers.Formal_Ordered_Maps with
  63   SPARK_Mode
  64 is
  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
1024 private
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
1052 end Ada.Containers.Formal_Ordered_Maps;