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