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