gcc/ada/a-cofove.ads

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