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