gcc/ada/a-cfinve.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --                 ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS                 --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2014-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 --  Similar to Ada.Containers.Formal_Vectors. The main difference is that
  33 --  Element_Type may be indefinite (but not an unconstrained array).
  34
  35 with Ada.Containers.Bounded_Holders;
  36 with Ada.Containers.Functional_Vectors;
  37
  38 generic
  39    type Index_Type is range <>;
  40    type Element_Type (<>) is private;
  41    Max_Size_In_Storage_Elements : Natural :=
  42                                     Element_Type'Max_Size_In_Storage_Elements;
  43    --  Maximum size of Vector elements in bytes. This has the same meaning as
  44    --  in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
  45    --  setting this too small can lead to erroneous execution; see comments in
  46    --  Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
  47    --  responsibility of clients to calculate the maximum size of all types in
  48    --  the class.
  49
  50    Bounded : Boolean := True;
  51    --  If True, the containers are bounded; the initial capacity is the maximum
  52    --  size, and heap allocation will be avoided. If False, the containers can
  53    --  grow via heap allocation.
  54
  55 package Ada.Containers.Formal_Indefinite_Vectors with
  56   SPARK_Mode => On
  57 is
  58    pragma Annotate (CodePeer, Skip_Analysis);
  59
  60    subtype Extended_Index is Index_Type'Base
  61    range Index_Type'First - 1 ..
  62      Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
  63
  64    No_Index : constant Extended_Index := Extended_Index'First;
  65
  66    subtype Capacity_Range is
  67      Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
  68
  69    type Vector (Capacity : Capacity_Range) is limited private with
  70      Default_Initial_Condition => Is_Empty (Vector);
  71    --  In the bounded case, Capacity is the capacity of the container, which
  72    --  never changes. In the unbounded case, Capacity is the initial capacity
  73    --  of the container, and operations such as Reserve_Capacity and Append can
  74    --  increase the capacity. The capacity never shrinks, except in the case of
  75    --  Clear.
  76    --
  77    --  Note that all objects of type Vector are constrained, including in the
  78    --  unbounded case; you can't assign from one object to another if the
  79    --  Capacity is different.
  80
  81    function Length (Container : Vector) return Capacity_Range with
  82      Global => null,
  83      Post   => Length'Result <= Capacity (Container);
  84
  85    pragma Unevaluated_Use_Of_Old (Allow);
  86
  87    package Formal_Model with Ghost is
  88
  89       package M is new Ada.Containers.Functional_Vectors
  90         (Index_Type   => Index_Type,
  91          Element_Type => Element_Type);
  92
  93       function "="
  94         (Left  : M.Sequence;
  95          Right : M.Sequence) return Boolean renames M."=";
  96
  97       function "<"
  98         (Left  : M.Sequence;
  99          Right : M.Sequence) return Boolean renames M."<";
 100
 101       function "<="
 102         (Left  : M.Sequence;
 103          Right : M.Sequence) return Boolean renames M."<=";
 104
 105       function M_Elements_In_Union
 106         (Container : M.Sequence;
 107          Left      : M.Sequence;
 108          Right     : M.Sequence) return Boolean
 109       --  The elements of Container are contained in either Left or Right
 110       with
 111         Global => null,
 112         Post   =>
 113           M_Elements_In_Union'Result =
 114             (for all I in Index_Type'First .. M.Last (Container) =>
 115               (for some J in Index_Type'First .. M.Last (Left) =>
 116                 Element (Container, I) = Element (Left, J))
 117               or (for some J in Index_Type'First .. M.Last (Right) =>
 118                     Element (Container, I) = Element (Right, J)));
 119       pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
 120
 121       function M_Elements_Included
 122         (Left  : M.Sequence;
 123          L_Fst : Index_Type := Index_Type'First;
 124          L_Lst : Extended_Index;
 125          Right : M.Sequence;
 126          R_Fst : Index_Type := Index_Type'First;
 127          R_Lst : Extended_Index) return Boolean
 128       --  The elements of the slice from L_Fst to L_Lst in Left are contained
 129       --  in the slide from R_Fst to R_Lst in Right.
 130       with
 131         Global => null,
 132         Pre    => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
 133         Post   =>
 134           M_Elements_Included'Result =
 135             (for all I in L_Fst .. L_Lst =>
 136               (for some J in R_Fst .. R_Lst =>
 137                 Element (Left, I) = Element (Right, J)));
 138       pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
 139
 140       function M_Elements_Reversed
 141         (Left  : M.Sequence;
 142          Right : M.Sequence) return Boolean
 143       --  Right is Left in reverse order
 144       with
 145         Global => null,
 146         Post   =>
 147           M_Elements_Reversed'Result =
 148             (M.Length (Left) = M.Length (Right)
 149               and (for all I in Index_Type'First .. M.Last (Left) =>
 150                      Element (Left, I) =
 151                      Element (Right, M.Last (Left) - I + 1))
 152               and (for all I in Index_Type'First .. M.Last (Right) =>
 153                      Element (Right, I) =
 154                      Element (Left, M.Last (Left) - I + 1)));
 155       pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
 156
 157       function M_Elements_Swapped
 158         (Left  : M.Sequence;
 159          Right : M.Sequence;
 160          X     : Index_Type;
 161          Y     : Index_Type) return Boolean
 162       --  Elements stored at X and Y are reversed in Left and Right
 163       with
 164         Global => null,
 165         Pre    => X <= M.Last (Left) and Y <= M.Last (Left),
 166         Post   =>
 167           M_Elements_Swapped'Result =
 168             (M.Length (Left) = M.Length (Right)
 169               and Element (Left, X) = Element (Right, Y)
 170               and Element (Left, Y) = Element (Right, X)
 171               and M.Equal_Except (Left, Right, X, Y));
 172       pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
 173
 174       function Model (Container : Vector) return M.Sequence with
 175       --  The high-level model of a vector is a sequence of elements. The
 176       --  sequence really is similar to the vector itself. However, it is not
 177       --  limited which allows usage of 'Old and 'Loop_Entry attributes.
 178
 179         Ghost,
 180         Global => null,
 181         Post   => M.Length (Model'Result) = Length (Container);
 182
 183       function Element
 184         (S : M.Sequence;
 185          I : Index_Type) return Element_Type renames M.Get;
 186       --  To improve readability of contracts, we rename the function used to
 187       --  access an element in the model to Element.
 188    end Formal_Model;
 189    use Formal_Model;
 190
 191    function Empty_Vector return Vector with
 192      Global => null,
 193      Post   => Length (Empty_Vector'Result) = 0;
 194
 195    function "=" (Left, Right : Vector) return Boolean with
 196      Global => null,
 197      Post   => "="'Result = (Model (Left) = Model (Right));
 198
 199    function To_Vector
 200      (New_Item : Element_Type;
 201       Length   : Capacity_Range) return Vector
 202    with
 203      Global => null,
 204      Post   =>
 205        Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length
 206          and M.Constant_Range (Container => Model (To_Vector'Result),
 207                                Fst       => Index_Type'First,
 208                                Lst       => Last_Index (To_Vector'Result),
 209                                Item      => New_Item);
 210
 211    function Capacity (Container : Vector) return Capacity_Range with
 212      Global => null,
 213      Post   =>
 214        Capacity'Result = (if Bounded then Container.Capacity
 215                           else Capacity_Range'Last);
 216    pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
 217
 218    procedure Reserve_Capacity
 219      (Container : in out Vector;
 220       Capacity  : Capacity_Range)
 221    with
 222      Global => null,
 223      Pre    => (if Bounded then Capacity <= Container.Capacity),
 224      Post   => Model (Container) = Model (Container)'Old;
 225
 226    function Is_Empty (Container : Vector) return Boolean with
 227      Global => null,
 228      Post   => Is_Empty'Result = (Length (Container) = 0);
 229
 230    procedure Clear (Container : in out Vector) with
 231      Global => null,
 232      Post   => Length (Container) = 0;
 233    --  Note that this reclaims storage in the unbounded case. You need to call
 234    --  this before a container goes out of scope in order to avoid storage
 235    --  leaks. In addition, "X := ..." can leak unless you Clear(X) first.
 236
 237    procedure Assign (Target : in out Vector; Source : Vector) with
 238      Global => null,
 239      Pre    => (if Bounded then Length (Source) <= Target.Capacity),
 240      Post   => Model (Target) = Model (Source);
 241
 242    function Copy
 243      (Source   : Vector;
 244       Capacity : Capacity_Range := 0) return Vector
 245    with
 246      Global => null,
 247      Pre    => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
 248      Post   =>
 249        Model (Copy'Result) = Model (Source)
 250          and (if Capacity = 0 then Copy'Result.Capacity = Length (Source)
 251               else Copy'Result.Capacity = Capacity);
 252
 253    procedure Move (Target : in out Vector; Source : in out Vector)
 254    with
 255      Global => null,
 256      Pre    => (if Bounded then Length (Source) <= Capacity (Target)),
 257      Post   => Model (Target) = Model (Source)'Old and Length (Source) = 0;
 258
 259    function Element
 260      (Container : Vector;
 261       Index     : Index_Type) return Element_Type
 262    with
 263      Global => null,
 264      Pre    => Index in First_Index (Container) .. Last_Index (Container),
 265      Post   => Element'Result = Element (Model (Container), Index);
 266    pragma Annotate (GNATprove, Inline_For_Proof, Element);
 267
 268    procedure Replace_Element
 269      (Container : in out Vector;
 270       Index     : Index_Type;
 271       New_Item  : Element_Type)
 272    with
 273      Global => null,
 274      Pre    => Index in First_Index (Container) .. Last_Index (Container),
 275      Post   =>
 276        Length (Container) = Length (Container)'Old
 277
 278          --  Container now has New_Item at index Index
 279
 280          and Element (Model (Container), Index) = New_Item
 281
 282          --  All other elements are preserved
 283
 284          and M.Equal_Except
 285                (Left     => Model (Container)'Old,
 286                 Right    => Model (Container),
 287                 Position => Index);
 288
 289    procedure Insert
 290      (Container : in out Vector;
 291       Before    : Extended_Index;
 292       New_Item  : Vector)
 293    with
 294      Global => null,
 295      Pre    =>
 296        Length (Container) <= Capacity (Container) - Length (New_Item)
 297          and (Before in Index_Type'First .. Last_Index (Container)
 298               or Before - 1 = Last_Index (Container)),
 299      Post   =>
 300        Length (Container) = Length (Container)'Old + Length (New_Item)
 301
 302          --  Elements located before Before in Container are preserved
 303
 304          and M.Range_Equal
 305                (Left  => Model (Container)'Old,
 306                 Right => Model (Container),
 307                 Fst   => Index_Type'First,
 308                 Lst   => Before - 1)
 309
 310          --  Elements of New_Item are inserted at position Before
 311
 312          and (if Length (New_Item) > 0 then
 313                 M.Range_Shifted
 314                   (Left   => Model (New_Item),
 315                     Right  => Model (Container),
 316                     Fst    => Index_Type'First,
 317                     Lst    => Last_Index (New_Item),
 318                     Offset => Count_Type (Before - Index_Type'First)))
 319
 320          --  Elements located after Before in Container are shifted
 321
 322          and M.Range_Shifted
 323                (Left   => Model (Container)'Old,
 324                 Right  => Model (Container),
 325                 Fst    => Before,
 326                 Lst    => Last_Index (Container)'Old,
 327                 Offset => Length (New_Item));
 328
 329    procedure Insert
 330      (Container : in out Vector;
 331       Before    : Extended_Index;
 332       New_Item  : Element_Type)
 333    with
 334      Global => null,
 335      Pre    =>
 336        Length (Container) < Capacity (Container)
 337          and then (Before in Index_Type'First .. Last_Index (Container) + 1),
 338      Post   =>
 339        Length (Container) = Length (Container)'Old + 1
 340
 341          --  Elements located before Before in Container are preserved
 342
 343          and M.Range_Equal
 344                (Left  => Model (Container)'Old,
 345                 Right => Model (Container),
 346                 Fst   => Index_Type'First,
 347                 Lst   => Before - 1)
 348
 349          --  Container now has New_Item at index Before
 350
 351          and Element (Model (Container), Before) = New_Item
 352
 353          --  Elements located after Before in Container are shifted by 1
 354
 355          and M.Range_Shifted
 356                (Left   => Model (Container)'Old,
 357                 Right  => Model (Container),
 358                 Fst    => Before,
 359                 Lst    => Last_Index (Container)'Old,
 360                 Offset => 1);
 361
 362    procedure Insert
 363      (Container : in out Vector;
 364       Before    : Extended_Index;
 365       New_Item  : Element_Type;
 366       Count     : Count_Type)
 367    with
 368      Global => null,
 369      Pre    =>
 370        Length (Container) <= Capacity (Container) - Count
 371          and (Before in Index_Type'First .. Last_Index (Container)
 372               or Before - 1 = Last_Index (Container)),
 373      Post   =>
 374        Length (Container) = Length (Container)'Old + Count
 375
 376          --  Elements located before Before in Container are preserved
 377
 378          and M.Range_Equal
 379                (Left  => Model (Container)'Old,
 380                 Right => Model (Container),
 381                 Fst   => Index_Type'First,
 382                 Lst   => Before - 1)
 383
 384          --  New_Item is inserted Count times at position Before
 385
 386          and (if Count > 0 then
 387                 M.Constant_Range
 388                   (Container => Model (Container),
 389                     Fst       => Before,
 390                     Lst       => Before + Index_Type'Base (Count - 1),
 391                     Item      => New_Item))
 392
 393          --  Elements located after Before in Container are shifted
 394
 395          and M.Range_Shifted
 396                (Left   => Model (Container)'Old,
 397                 Right  => Model (Container),
 398                 Fst    => Before,
 399                 Lst    => Last_Index (Container)'Old,
 400                 Offset => Count);
 401
 402    procedure Prepend
 403      (Container : in out Vector;
 404       New_Item  : Vector)
 405    with
 406      Global => null,
 407      Pre    => Length (Container) <= Capacity (Container) - Length (New_Item),
 408      Post   =>
 409        Length (Container) = Length (Container)'Old + Length (New_Item)
 410
 411          --  Elements of New_Item are inserted at the beginning of Container
 412
 413          and M.Range_Equal
 414                (Left  => Model (New_Item),
 415                 Right => Model (Container),
 416                 Fst   => Index_Type'First,
 417                 Lst   => Last_Index (New_Item))
 418
 419          --  Elements of Container are shifted
 420
 421          and M.Range_Shifted
 422                (Left   => Model (Container)'Old,
 423                 Right  => Model (Container),
 424                 Fst    => Index_Type'First,
 425                 Lst    => Last_Index (Container)'Old,
 426                 Offset => Length (New_Item));
 427
 428    procedure Prepend
 429      (Container : in out Vector;
 430       New_Item  : Element_Type)
 431    with
 432      Global => null,
 433      Pre    => Length (Container) < Capacity (Container),
 434      Post   =>
 435        Length (Container) = Length (Container)'Old + 1
 436
 437          --  Container now has New_Item at Index_Type'First
 438
 439          and Element (Model (Container), Index_Type'First) = New_Item
 440
 441          --  Elements of Container are shifted by 1
 442
 443          and M.Range_Shifted
 444                (Left   => Model (Container)'Old,
 445                 Right  => Model (Container),
 446                 Fst    => Index_Type'First,
 447                 Lst    => Last_Index (Container)'Old,
 448                 Offset => 1);
 449
 450    procedure Prepend
 451      (Container : in out Vector;
 452       New_Item  : Element_Type;
 453       Count     : Count_Type)
 454    with
 455      Global => null,
 456      Pre    => Length (Container) <= Capacity (Container) - Count,
 457      Post   =>
 458        Length (Container) = Length (Container)'Old + Count
 459
 460          --  New_Item is inserted Count times at the beginning of Container
 461
 462          and M.Constant_Range
 463                (Container => Model (Container),
 464                 Fst       => Index_Type'First,
 465                 Lst       => Index_Type'First + Index_Type'Base (Count - 1),
 466                 Item      => New_Item)
 467
 468          --  Elements of Container are shifted
 469
 470          and M.Range_Shifted
 471                (Left   => Model (Container)'Old,
 472                 Right  => Model (Container),
 473                 Fst    => Index_Type'First,
 474                 Lst    => Last_Index (Container)'Old,
 475                 Offset => Count);
 476
 477    procedure Append
 478      (Container : in out Vector;
 479       New_Item  : Vector)
 480    with
 481      Global         => null,
 482      Pre            =>
 483        Length (Container) <= Capacity (Container) - Length (New_Item),
 484      Post           =>
 485        Length (Container) = Length (Container)'Old + Length (New_Item)
 486
 487          --  The elements of Container are preserved
 488
 489          and Model (Container)'Old <= Model (Container)
 490
 491          --  Elements of New_Item are inserted at the end of Container
 492
 493          and (if Length (New_Item) > 0 then
 494                 M.Range_Shifted
 495                  (Left   => Model (New_Item),
 496                    Right  => Model (Container),
 497                    Fst    => Index_Type'First,
 498                    Lst    => Last_Index (New_Item),
 499                    Offset =>
 500                      Count_Type
 501                        (Last_Index (Container)'Old - Index_Type'First + 1)));
 502
 503    procedure Append
 504      (Container : in out Vector;
 505       New_Item  : Element_Type)
 506    with
 507      Global => null,
 508      Pre    => Length (Container) < Capacity (Container),
 509      Post   =>
 510        Length (Container) = Length (Container)'Old + 1
 511
 512          --  Elements of Container are preserved
 513
 514          and Model (Container)'Old < Model (Container)
 515
 516          --  Container now has New_Item at the end of Container
 517
 518          and Element
 519                (Model (Container), Last_Index (Container)'Old + 1) = New_Item;
 520
 521    procedure Append
 522      (Container : in out Vector;
 523       New_Item  : Element_Type;
 524       Count     : Count_Type)
 525    with
 526      Global => null,
 527      Pre    => Length (Container) <= Capacity (Container) - Count,
 528      Post   =>
 529        Length (Container) = Length (Container)'Old + Count
 530
 531          --  Elements of Container are preserved
 532
 533          and Model (Container)'Old <= Model (Container)
 534
 535          --  New_Item is inserted Count times at the end of Container
 536
 537          and (if Count > 0 then
 538                 M.Constant_Range
 539                   (Container => Model (Container),
 540                     Fst       => Last_Index (Container)'Old + 1,
 541                     Lst       =>
 542                       Last_Index (Container)'Old + Index_Type'Base (Count),
 543                     Item      => New_Item));
 544
 545    procedure Delete
 546      (Container : in out Vector;
 547       Index     : Extended_Index)
 548    with
 549      Global => null,
 550      Pre    => Index in First_Index (Container) .. Last_Index (Container),
 551      Post   =>
 552        Length (Container) = Length (Container)'Old - 1
 553
 554          --  Elements located before Index in Container are preserved
 555
 556          and M.Range_Equal
 557                (Left  => Model (Container)'Old,
 558                 Right => Model (Container),
 559                 Fst   => Index_Type'First,
 560                 Lst   => Index - 1)
 561
 562          --  Elements located after Index in Container are shifted by 1
 563
 564          and M.Range_Shifted
 565                (Left   => Model (Container),
 566                 Right  => Model (Container)'Old,
 567                 Fst    => Index,
 568                 Lst    => Last_Index (Container),
 569                 Offset => 1);
 570
 571    procedure Delete
 572      (Container : in out Vector;
 573       Index     : Extended_Index;
 574       Count     : Count_Type)
 575    with
 576      Global         => null,
 577      Pre            =>
 578        Index in First_Index (Container) .. Last_Index (Container),
 579      Post           =>
 580        Length (Container) in
 581          Length (Container)'Old - Count .. Length (Container)'Old
 582
 583          --  The elements of Container located before Index are preserved.
 584
 585          and M.Range_Equal
 586                (Left  => Model (Container)'Old,
 587                 Right => Model (Container),
 588                 Fst   => Index_Type'First,
 589                 Lst   => Index - 1),
 590
 591      Contract_Cases =>
 592
 593        --  All the elements after Position have been erased
 594
 595        (Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
 596           Length (Container) = Count_Type (Index - Index_Type'First),
 597
 598         others =>
 599           Length (Container) = Length (Container)'Old - Count
 600
 601             --  Other elements are shifted by Count
 602
 603             and M.Range_Shifted
 604                   (Left   => Model (Container),
 605                    Right  => Model (Container)'Old,
 606                    Fst    => Index,
 607                    Lst    => Last_Index (Container),
 608                    Offset => Count));
 609
 610    procedure Delete_First
 611      (Container : in out Vector)
 612    with
 613      Global => null,
 614      Pre    => Length (Container) > 0,
 615      Post   =>
 616        Length (Container) = Length (Container)'Old - 1
 617
 618          --  Elements of Container are shifted by 1
 619
 620          and M.Range_Shifted
 621                (Left   => Model (Container),
 622                 Right  => Model (Container)'Old,
 623                 Fst    => Index_Type'First,
 624                 Lst    => Last_Index (Container),
 625                 Offset => 1);
 626
 627    procedure Delete_First
 628      (Container : in out Vector;
 629       Count     : Count_Type)
 630    with
 631      Global         => null,
 632      Contract_Cases =>
 633
 634        --  All the elements of Container have been erased
 635
 636        (Length (Container) <= Count => Length (Container) = 0,
 637
 638         others =>
 639           Length (Container) = Length (Container)'Old - Count
 640
 641             --  Elements of Container are shifted by Count
 642
 643             and M.Range_Shifted
 644                   (Left   => Model (Container),
 645                    Right  => Model (Container)'Old,
 646                    Fst    => Index_Type'First,
 647                    Lst    => Last_Index (Container),
 648                    Offset => Count));
 649
 650    procedure Delete_Last
 651      (Container : in out Vector)
 652    with
 653      Global => null,
 654      Pre    => Length (Container) > 0,
 655      Post   =>
 656        Length (Container) = Length (Container)'Old - 1
 657
 658          --  Elements of Container are preserved
 659
 660          and Model (Container) < Model (Container)'Old;
 661
 662    procedure Delete_Last
 663      (Container : in out Vector;
 664       Count     : Count_Type)
 665    with
 666      Global         => null,
 667      Contract_Cases =>
 668
 669        --  All the elements after Position have been erased
 670
 671        (Length (Container) <= Count => Length (Container) = 0,
 672
 673         others =>
 674           Length (Container) = Length (Container)'Old - Count
 675
 676             --  The elements of Container are preserved
 677
 678             and Model (Container) <= Model (Container)'Old);
 679
 680    procedure Reverse_Elements (Container : in out Vector) with
 681      Global => null,
 682      Post   => M_Elements_Reversed (Model (Container)'Old, Model (Container));
 683
 684    procedure Swap (Container : in out Vector; I, J : Index_Type) with
 685      Global => null,
 686      Pre    => I in First_Index (Container) .. Last_Index (Container)
 687       and then J in First_Index (Container) .. Last_Index (Container),
 688      Post   =>
 689        M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
 690
 691    function First_Index (Container : Vector) return Index_Type with
 692      Global => null,
 693      Post   => First_Index'Result = Index_Type'First;
 694    pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
 695
 696    function First_Element (Container : Vector) return Element_Type with
 697      Global => null,
 698      Pre    => not Is_Empty (Container),
 699      Post   =>
 700        First_Element'Result = Element (Model (Container), Index_Type'First);
 701    pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
 702
 703    function Last_Index (Container : Vector) return Extended_Index with
 704      Global => null,
 705      Post   => Last_Index'Result = M.Last (Model (Container));
 706    pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
 707
 708    function Last_Element (Container : Vector) return Element_Type with
 709      Global => null,
 710      Pre    => not Is_Empty (Container),
 711      Post   =>
 712        Last_Element'Result =
 713          Element (Model (Container), Last_Index (Container));
 714    pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
 715
 716    function Find_Index
 717      (Container : Vector;
 718       Item      : Element_Type;
 719       Index     : Index_Type := Index_Type'First) return Extended_Index
 720    with
 721      Global         => null,
 722      Contract_Cases =>
 723
 724        --  If Item is not is not contained in Container after Index, Find_Index
 725        --  returns No_Index.
 726
 727        (Index > Last_Index (Container)
 728         or else not M.Contains
 729                      (Container => Model (Container),
 730                       Fst       => Index,
 731                       Lst       => Last_Index (Container),
 732                       Item      => Item)
 733         =>
 734           Find_Index'Result = No_Index,
 735
 736         --  Otherwise, Find_Index returns a valid index greater than Index
 737
 738         others =>
 739            Find_Index'Result in Index .. Last_Index (Container)
 740
 741             --  The element at this index in Container is Item
 742
 743             and Element (Model (Container), Find_Index'Result) = Item
 744
 745             --  It is the first occurrence of Item after Index in Container
 746
 747             and not M.Contains
 748                       (Container => Model (Container),
 749                        Fst       => Index,
 750                        Lst       => Find_Index'Result - 1,
 751                        Item      => Item));
 752
 753    function Reverse_Find_Index
 754      (Container : Vector;
 755       Item      : Element_Type;
 756       Index     : Index_Type := Index_Type'Last) return Extended_Index
 757    with
 758      Global         => null,
 759      Contract_Cases =>
 760
 761        --  If Item is not is not contained in Container before Index,
 762        --  Reverse_Find_Index returns No_Index.
 763
 764        (not M.Contains
 765               (Container => Model (Container),
 766                Fst       => Index_Type'First,
 767                Lst       => (if Index <= Last_Index (Container) then Index
 768                              else Last_Index (Container)),
 769                Item      => Item)
 770         =>
 771           Reverse_Find_Index'Result = No_Index,
 772
 773         --  Otherwise, Reverse_Find_Index returns a valid index smaller than
 774         --  Index
 775
 776         others =>
 777            Reverse_Find_Index'Result in Index_Type'First .. Index
 778             and Reverse_Find_Index'Result <= Last_Index (Container)
 779
 780             --  The element at this index in Container is Item
 781
 782             and Element (Model (Container), Reverse_Find_Index'Result) = Item
 783
 784             --  It is the last occurrence of Item before Index in Container
 785
 786             and not M.Contains
 787                       (Container => Model (Container),
 788                        Fst       => Reverse_Find_Index'Result + 1,
 789                        Lst       =>
 790                          (if Index <= Last_Index (Container) then Index
 791                           else Last_Index (Container)),
 792                        Item      => Item));
 793
 794    function Contains
 795      (Container : Vector;
 796       Item      : Element_Type) return Boolean
 797    with
 798      Global => null,
 799      Post   =>
 800        Contains'Result = M.Contains (Container => Model (Container),
 801                                      Fst       => Index_Type'First,
 802                                      Lst       => Last_Index (Container),
 803                                      Item      => Item);
 804
 805    function Has_Element
 806      (Container : Vector;
 807       Position  : Extended_Index) return Boolean
 808    with
 809      Global => null,
 810      Post   =>
 811        Has_Element'Result =
 812          (Position in Index_Type'First .. Last_Index (Container));
 813    pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
 814
 815    generic
 816       with function "<" (Left, Right : Element_Type) return Boolean is <>;
 817    package Generic_Sorting with SPARK_Mode is
 818       function M_Elements_Sorted (Container : M.Sequence) return Boolean with
 819         Ghost,
 820         Global => null,
 821         Post   =>
 822           M_Elements_Sorted'Result =
 823             (for all I in Index_Type'First .. M.Last (Container) =>
 824               (for all J in I .. M.Last (Container) =>
 825                  Element (Container, I) = Element (Container, J)
 826                    or Element (Container, I) < Element (Container, J)));
 827       pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
 828
 829       function Is_Sorted (Container : Vector) return Boolean with
 830         Global => null,
 831         Post   => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
 832
 833       procedure Sort (Container : in out Vector) with
 834         Global => null,
 835         Post   =>
 836           Length (Container) = Length (Container)'Old
 837             and M_Elements_Sorted (Model (Container))
 838             and M_Elements_Included (Left  => Model (Container)'Old,
 839                                      L_Lst => Last_Index (Container),
 840                                      Right => Model (Container),
 841                                      R_Lst => Last_Index (Container))
 842             and M_Elements_Included (Left  => Model (Container),
 843                                      L_Lst => Last_Index (Container),
 844                                      Right => Model (Container)'Old,
 845                                      R_Lst => Last_Index (Container));
 846
 847       procedure Merge (Target : in out Vector; Source : in out Vector) with
 848       --  Target and Source should not be aliased
 849         Global => null,
 850         Pre    => Length (Source) <= Capacity (Target) - Length (Target),
 851         Post   =>
 852           Length (Target) = Length (Target)'Old + Length (Source)'Old
 853             and Length (Source) = 0
 854             and (if M_Elements_Sorted (Model (Target)'Old)
 855                    and M_Elements_Sorted (Model (Source)'Old)
 856                  then M_Elements_Sorted (Model (Target)))
 857             and M_Elements_Included (Left  => Model (Target)'Old,
 858                                      L_Lst => Last_Index (Target)'Old,
 859                                      Right => Model (Target),
 860                                      R_Lst => Last_Index (Target))
 861             and M_Elements_Included (Left  => Model (Source)'Old,
 862                                      L_Lst => Last_Index (Source)'Old,
 863                                      Right => Model (Target),
 864                                      R_Lst => Last_Index (Target))
 865             and M_Elements_In_Union (Model (Target),
 866                                      Model (Source)'Old,
 867                                      Model (Target)'Old);
 868    end Generic_Sorting;
 869
 870 private
 871    pragma SPARK_Mode (Off);
 872
 873    pragma Inline (First_Index);
 874    pragma Inline (Last_Index);
 875    pragma Inline (Element);
 876    pragma Inline (First_Element);
 877    pragma Inline (Last_Element);
 878    pragma Inline (Replace_Element);
 879    pragma Inline (Contains);
 880
 881    --  The implementation method is to instantiate Bounded_Holders to get a
 882    --  definite type for Element_Type.
 883
 884    package Holders is new Bounded_Holders
 885      (Element_Type, Max_Size_In_Storage_Elements, "=");
 886    use Holders;
 887
 888    subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
 889    type Elements_Array is array (Array_Index range <>) of Holder;
 890    function "=" (L, R : Elements_Array) return Boolean is abstract;
 891
 892    type Elements_Array_Ptr is access all Elements_Array;
 893
 894    type Vector (Capacity : Capacity_Range) is limited record
 895       --  In the bounded case, the elements are stored in Elements. In the
 896       --  unbounded case, the elements are initially stored in Elements, until
 897       --  we run out of room, then we switch to Elements_Ptr.
 898       Last         : Extended_Index := No_Index;
 899       Elements_Ptr : Elements_Array_Ptr := null;
 900       Elements     : aliased Elements_Array (1 .. Capacity);
 901    end record;
 902
 903    --  The primary reason Vector is limited is that in the unbounded case, once
 904    --  Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
 905    --  cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
 906    --  so for example "Append (X, ...);" will modify BOTH X and Y. That would
 907    --  allow SPARK to "prove" things that are false. We could fix that by
 908    --  making Vector a controlled type, and override Adjust to make a deep
 909    --  copy, but finalization is not allowed in SPARK.
 910    --
 911    --  Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
 912    --  allowed on Vectors.
 913
 914    function Empty_Vector return Vector is
 915      ((Capacity => 0, others => <>));
 916
 917 end Ada.Containers.Formal_Indefinite_Vectors;