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