gcc/ada/a-cfdlli.ads

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