gcc/ada/libgnat/a-cforse.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 _ O R D E R E D _ S E T 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_Ordered_Sets in
  33 --  the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
  34 --  making it easier to express properties, and by making the specification of
  35 --  this 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 --  The modifications are:
  39
  40 --    A parameter for the container is added to every function reading the
  41 --    content of a container: Key, Element, Next, Query_Element, Previous,
  42 --    Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
  43 --    need to have cursors which are valid on different containers (typically
  44 --    a container C and its previous version C'Old) for expressing properties,
  45 --    which is not possible if cursors encapsulate an access to the underlying
  46 --    container. The operators "<" and ">" that could not be modified that way
  47 --    have been removed.
  48
  49 with Ada.Containers.Functional_Maps;
  50 with Ada.Containers.Functional_Sets;
  51 with Ada.Containers.Functional_Vectors;
  52 private with Ada.Containers.Red_Black_Trees;
  53
  54 generic
  55    type Element_Type is private;
  56
  57    with function "<" (Left, Right : Element_Type) return Boolean is <>;
  58
  59 package Ada.Containers.Formal_Ordered_Sets with
  60   SPARK_Mode
  61 is
  62    pragma Annotate (CodePeer, Skip_Analysis);
  63
  64    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
  65    with
  66      Global => null,
  67      Post   =>
  68        Equivalent_Elements'Result =
  69          (not (Left < Right) and not (Right < Left));
  70    pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements);
  71
  72    type Set (Capacity : Count_Type) is private with
  73      Iterable => (First       => First,
  74                   Next        => Next,
  75                   Has_Element => Has_Element,
  76                   Element     => Element),
  77      Default_Initial_Condition => Is_Empty (Set);
  78    pragma Preelaborable_Initialization (Set);
  79
  80    type Cursor is record
  81       Node : Count_Type;
  82    end record;
  83
  84    No_Element : constant Cursor := (Node => 0);
  85
  86    function Length (Container : Set) return Count_Type with
  87      Global => null,
  88      Post   => Length'Result <= Container.Capacity;
  89
  90    pragma Unevaluated_Use_Of_Old (Allow);
  91
  92    package Formal_Model with Ghost is
  93       subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
  94
  95       package M is new Ada.Containers.Functional_Sets
  96         (Element_Type    => Element_Type,
  97          Equivalent_Elements => Equivalent_Elements);
  98
  99       function "="
 100         (Left  : M.Set;
 101          Right : M.Set) return Boolean renames M."=";
 102
 103       function "<="
 104         (Left  : M.Set;
 105          Right : M.Set) return Boolean renames M."<=";
 106
 107       package E is new Ada.Containers.Functional_Vectors
 108         (Element_Type => Element_Type,
 109          Index_Type   => Positive_Count_Type);
 110
 111       function "="
 112         (Left  : E.Sequence;
 113          Right : E.Sequence) return Boolean renames E."=";
 114
 115       function "<"
 116         (Left  : E.Sequence;
 117          Right : E.Sequence) return Boolean renames E."<";
 118
 119       function "<="
 120         (Left  : E.Sequence;
 121          Right : E.Sequence) return Boolean renames E."<=";
 122
 123       function E_Bigger_Than_Range
 124         (Container : E.Sequence;
 125          Fst       : Positive_Count_Type;
 126          Lst       : Count_Type;
 127          Item      : Element_Type) return Boolean
 128       with
 129         Global => null,
 130         Pre    => Lst <= E.Length (Container),
 131         Post   =>
 132           E_Bigger_Than_Range'Result =
 133             (for all I in Fst .. Lst => E.Get (Container, I) < Item);
 134       pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
 135
 136       function E_Smaller_Than_Range
 137         (Container : E.Sequence;
 138          Fst       : Positive_Count_Type;
 139          Lst       : Count_Type;
 140          Item      : Element_Type) return Boolean
 141       with
 142         Global => null,
 143         Pre    => Lst <= E.Length (Container),
 144         Post   =>
 145           E_Smaller_Than_Range'Result =
 146             (for all I in Fst .. Lst => Item < E.Get (Container, I));
 147       pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
 148
 149       function E_Is_Find
 150         (Container : E.Sequence;
 151          Item      : Element_Type;
 152          Position  : Count_Type) return Boolean
 153       with
 154         Global => null,
 155         Pre    => Position - 1 <= E.Length (Container),
 156         Post   =>
 157           E_Is_Find'Result =
 158
 159             ((if Position > 0 then
 160                 E_Bigger_Than_Range (Container, 1, Position - 1, Item))
 161
 162              and (if Position < E.Length (Container) then
 163                     E_Smaller_Than_Range
 164                       (Container,
 165                        Position + 1,
 166                        E.Length (Container),
 167                        Item)));
 168       pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
 169
 170       function Find
 171         (Container : E.Sequence;
 172          Item      : Element_Type) return Count_Type
 173       --  Search for Item in Container
 174
 175       with
 176         Global => null,
 177         Post =>
 178           (if Find'Result > 0 then
 179              Find'Result <= E.Length (Container)
 180                and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
 181
 182       function E_Elements_Included
 183         (Left  : E.Sequence;
 184          Right : E.Sequence) return Boolean
 185       --  The elements of Left are contained in Right
 186
 187       with
 188         Global => null,
 189         Post   =>
 190           E_Elements_Included'Result =
 191             (for all I in 1 .. E.Length (Left) =>
 192                Find (Right, E.Get (Left, I)) > 0
 193                  and then E.Get (Right, Find (Right, E.Get (Left, I))) =
 194                      E.Get (Left, I));
 195       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 196
 197       function E_Elements_Included
 198         (Left  : E.Sequence;
 199          Model : M.Set;
 200          Right : E.Sequence) return Boolean
 201       --  The elements of Container contained in Model are in Right
 202
 203       with
 204         Global => null,
 205         Post   =>
 206           E_Elements_Included'Result =
 207             (for all I in 1 .. E.Length (Left) =>
 208               (if M.Contains (Model, E.Get (Left, I)) then
 209                  Find (Right, E.Get (Left, I)) > 0
 210                    and then E.Get (Right, Find (Right, E.Get (Left, I))) =
 211                        E.Get (Left, I)));
 212       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 213
 214       function E_Elements_Included
 215         (Container : E.Sequence;
 216          Model     : M.Set;
 217          Left      : E.Sequence;
 218          Right     : E.Sequence) return Boolean
 219       --  The elements of Container contained in Model are in Left and others
 220       --  are in Right.
 221
 222       with
 223         Global => null,
 224         Post   =>
 225           E_Elements_Included'Result =
 226             (for all I in 1 .. E.Length (Container) =>
 227               (if M.Contains (Model, E.Get (Container, I)) then
 228                  Find (Left, E.Get (Container, I)) > 0
 229                    and then E.Get (Left, Find (Left, E.Get (Container, I))) =
 230                        E.Get (Container, I)
 231                else
 232                  Find (Right, E.Get (Container, I)) > 0
 233                    and then E.Get (Right, Find (Right, E.Get (Container, I))) =
 234                        E.Get (Container, I)));
 235       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 236
 237       package P is new Ada.Containers.Functional_Maps
 238         (Key_Type                       => Cursor,
 239          Element_Type                   => Positive_Count_Type,
 240          Equivalent_Keys                => "=",
 241          Enable_Handling_Of_Equivalence => False);
 242
 243       function "="
 244         (Left  : P.Map;
 245          Right : P.Map) return Boolean renames P."=";
 246
 247       function "<="
 248         (Left  : P.Map;
 249          Right : P.Map) return Boolean renames P."<=";
 250
 251       function P_Positions_Shifted
 252         (Small : P.Map;
 253          Big   : P.Map;
 254          Cut   : Positive_Count_Type;
 255          Count : Count_Type := 1) return Boolean
 256       with
 257         Global => null,
 258         Post   =>
 259           P_Positions_Shifted'Result =
 260
 261             --  Big contains all cursors of Small
 262
 263             (P.Keys_Included (Small, Big)
 264
 265               --  Cursors located before Cut are not moved, cursors located
 266               --  after are shifted by Count.
 267
 268               and (for all I of Small =>
 269                     (if P.Get (Small, I) < Cut then
 270                         P.Get (Big, I) = P.Get (Small, I)
 271                      else
 272                         P.Get (Big, I) - Count = P.Get (Small, I)))
 273
 274               --  New cursors of Big (if any) are between Cut and Cut - 1 +
 275               --  Count.
 276
 277               and (for all I of Big =>
 278                     P.Has_Key (Small, I)
 279                       or P.Get (Big, I) - Count in Cut - Count  .. Cut - 1));
 280
 281       function Mapping_Preserved
 282         (E_Left  : E.Sequence;
 283          E_Right : E.Sequence;
 284          P_Left  : P.Map;
 285          P_Right : P.Map) return Boolean
 286       with
 287         Ghost,
 288         Global => null,
 289         Post   =>
 290           (if Mapping_Preserved'Result then
 291
 292              --  Right contains all the cursors of Left
 293
 294              P.Keys_Included (P_Left, P_Right)
 295
 296                --  Right contains all the elements of Left
 297
 298                and E_Elements_Included (E_Left, E_Right)
 299
 300                --  Mappings from cursors to elements induced by E_Left, P_Left
 301                --  and E_Right, P_Right are the same.
 302
 303                and (for all C of P_Left =>
 304                      E.Get (E_Left, P.Get (P_Left, C)) =
 305                      E.Get (E_Right, P.Get (P_Right, C))));
 306
 307       function Mapping_Preserved_Except
 308         (E_Left   : E.Sequence;
 309          E_Right  : E.Sequence;
 310          P_Left   : P.Map;
 311          P_Right  : P.Map;
 312          Position : Cursor) return Boolean
 313       with
 314         Ghost,
 315         Global => null,
 316         Post   =>
 317           (if Mapping_Preserved_Except'Result then
 318
 319              --  Right contains all the cursors of Left
 320
 321              P.Keys_Included (P_Left, P_Right)
 322
 323                --  Mappings from cursors to elements induced by E_Left, P_Left
 324                --  and E_Right, P_Right are the same except for Position.
 325
 326                and (for all C of P_Left =>
 327                      (if C /= Position then
 328                         E.Get (E_Left, P.Get (P_Left, C)) =
 329                         E.Get (E_Right, P.Get (P_Right, C)))));
 330
 331       function Model (Container : Set) return M.Set with
 332       --  The high-level model of a set is a set of elements. Neither cursors
 333       --  nor order of elements are represented in this model. Elements are
 334       --  modeled up to equivalence.
 335
 336         Ghost,
 337         Global => null,
 338         Post   => M.Length (Model'Result) = Length (Container);
 339
 340       function Elements (Container : Set) return E.Sequence with
 341       --  The Elements sequence represents the underlying list structure of
 342       --  sets that is used for iteration. It stores the actual values of
 343       --  elements in the set. It does not model cursors.
 344
 345         Ghost,
 346         Global => null,
 347         Post   =>
 348           E.Length (Elements'Result) = Length (Container)
 349
 350             --  It only contains keys contained in Model
 351
 352             and (for all Item of Elements'Result =>
 353                    M.Contains (Model (Container), Item))
 354
 355             --  It contains all the elements contained in Model
 356
 357             and (for all Item of Model (Container) =>
 358                   (Find (Elements'Result, Item) > 0
 359                      and then Equivalent_Elements
 360                       (E.Get (Elements'Result, Find (Elements'Result, Item)),
 361                        Item)))
 362
 363             --  It is sorted in increasing order
 364
 365             and (for all I in 1 .. Length (Container) =>
 366                   Find (Elements'Result, E.Get (Elements'Result, I)) = I
 367                   and
 368                     E_Is_Find
 369                       (Elements'Result, E.Get (Elements'Result, I), I));
 370       pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
 371
 372       function Positions (Container : Set) return P.Map with
 373       --  The Positions map is used to model cursors. It only contains valid
 374       --  cursors and maps them to their position in the container.
 375
 376         Ghost,
 377         Global => null,
 378         Post   =>
 379           not P.Has_Key (Positions'Result, No_Element)
 380
 381             --  Positions of cursors are smaller than the container's length
 382
 383             and then
 384               (for all I of Positions'Result =>
 385                 P.Get (Positions'Result, I) in 1 .. Length (Container)
 386
 387             --  No two cursors have the same position. Note that we do not
 388             --  state that there is a cursor in the map for each position, as
 389             --  it is rarely needed.
 390
 391             and then
 392               (for all J of Positions'Result =>
 393                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
 394                   then I = J)));
 395
 396       procedure Lift_Abstraction_Level (Container : Set) with
 397         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
 398         --  assume that we can access the same elements by iterating over
 399         --  positions or cursors.
 400         --  This information is not generally useful except when switching from
 401         --  a low-level, cursor-aware view of a container, to a high-level,
 402         --  position-based view.
 403
 404         Ghost,
 405         Global => null,
 406         Post   =>
 407           (for all Item of Elements (Container) =>
 408             (for some I of Positions (Container) =>
 409               E.Get (Elements (Container), P.Get (Positions (Container), I)) =
 410                 Item));
 411
 412       function Contains
 413         (C : M.Set;
 414          K : Element_Type) return Boolean renames M.Contains;
 415       --  To improve readability of contracts, we rename the function used to
 416       --  search for an element in the model to Contains.
 417
 418    end Formal_Model;
 419    use Formal_Model;
 420
 421    Empty_Set : constant Set;
 422
 423    function "=" (Left, Right : Set) return Boolean with
 424      Global => null,
 425      Post   =>
 426
 427        --  If two sets are equal, they contain the same elements in the same
 428        --  order.
 429
 430        (if "="'Result then Elements (Left) = Elements (Right)
 431
 432         --  If they are different, then they do not contain the same elements
 433
 434         else
 435            not E_Elements_Included (Elements (Left), Elements (Right))
 436               or not E_Elements_Included (Elements (Right), Elements (Left)));
 437
 438    function Equivalent_Sets (Left, Right : Set) return Boolean with
 439      Global => null,
 440      Post   => Equivalent_Sets'Result = (Model (Left) = Model (Right));
 441
 442    function To_Set (New_Item : Element_Type) return Set with
 443      Global => null,
 444      Post   =>
 445        M.Is_Singleton (Model (To_Set'Result), New_Item)
 446          and Length (To_Set'Result) = 1
 447          and E.Get (Elements (To_Set'Result), 1) = New_Item;
 448
 449    function Is_Empty (Container : Set) return Boolean with
 450      Global => null,
 451      Post   => Is_Empty'Result = (Length (Container) = 0);
 452
 453    procedure Clear (Container : in out Set) with
 454      Global => null,
 455      Post   => Length (Container) = 0 and M.Is_Empty (Model (Container));
 456
 457    procedure Assign (Target : in out Set; Source : Set) with
 458      Global => null,
 459      Pre => Target.Capacity >= Length (Source),
 460      Post   =>
 461        Model (Target) = Model (Source)
 462          and Elements (Target) = Elements (Source)
 463          and Length (Target) = Length (Source);
 464
 465    function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
 466      Global => null,
 467      Pre    => Capacity = 0 or else Capacity >= Source.Capacity,
 468      Post   =>
 469        Model (Copy'Result) = Model (Source)
 470          and Elements (Copy'Result) = Elements (Source)
 471          and Positions (Copy'Result) = Positions (Source)
 472          and (if Capacity = 0 then
 473                  Copy'Result.Capacity = Source.Capacity
 474               else
 475                  Copy'Result.Capacity = Capacity);
 476
 477    function Element
 478      (Container : Set;
 479       Position  : Cursor) return Element_Type
 480    with
 481      Global => null,
 482      Pre    => Has_Element (Container, Position),
 483      Post   =>
 484        Element'Result =
 485          E.Get (Elements (Container), P.Get (Positions (Container), Position));
 486    pragma Annotate (GNATprove, Inline_For_Proof, Element);
 487
 488    procedure Replace_Element
 489      (Container : in out Set;
 490       Position  : Cursor;
 491       New_Item  : Element_Type)
 492    with
 493      Global => null,
 494      Pre    => Has_Element (Container, Position),
 495      Post   =>
 496        Length (Container) = Length (Container)'Old
 497
 498           --  Position now maps to New_Item
 499
 500           and Element (Container, Position) = New_Item
 501
 502           --  New_Item is contained in Container
 503
 504           and Contains (Model (Container), New_Item)
 505
 506           --  Other elements are preserved
 507
 508           and M.Included_Except
 509                 (Model (Container)'Old,
 510                  Model (Container),
 511                  Element (Container, Position)'Old)
 512           and M.Included_Except
 513                 (Model (Container),
 514                  Model (Container)'Old,
 515                  New_Item)
 516
 517           --  Mapping from cursors to elements is preserved
 518
 519           and Mapping_Preserved_Except
 520                 (E_Left   => Elements (Container)'Old,
 521                  E_Right  => Elements (Container),
 522                  P_Left   => Positions (Container)'Old,
 523                  P_Right  => Positions (Container),
 524                  Position => Position)
 525           and Positions (Container) = Positions (Container)'Old;
 526
 527    procedure Move (Target : in out Set; Source : in out Set) with
 528      Global => null,
 529      Pre    => Target.Capacity >= Length (Source),
 530      Post   =>
 531        Model (Target) = Model (Source)'Old
 532          and Elements (Target) = Elements (Source)'Old
 533          and Length (Source)'Old = Length (Target)
 534          and Length (Source) = 0;
 535
 536    procedure Insert
 537      (Container : in out Set;
 538       New_Item  : Element_Type;
 539       Position  : out Cursor;
 540       Inserted  : out Boolean)
 541    with
 542      Global         => null,
 543      Pre            =>
 544        Length (Container) < Container.Capacity
 545          or Contains (Container, New_Item),
 546      Post           =>
 547        Contains (Container, New_Item)
 548          and Has_Element (Container, Position)
 549          and Equivalent_Elements (Element (Container, Position), New_Item)
 550          and E_Is_Find
 551                (Elements (Container),
 552                 New_Item,
 553                 P.Get (Positions (Container), Position)),
 554      Contract_Cases =>
 555
 556        --  If New_Item is already in Container, it is not modified and Inserted
 557        --  is set to False.
 558
 559        (Contains (Container, New_Item) =>
 560           not Inserted
 561             and Model (Container) = Model (Container)'Old
 562             and Elements (Container) = Elements (Container)'Old
 563             and Positions (Container) = Positions (Container)'Old,
 564
 565         --  Otherwise, New_Item is inserted in Container and Inserted is set to
 566         --  True
 567
 568         others =>
 569           Inserted
 570             and Length (Container) = Length (Container)'Old + 1
 571
 572             --  Position now maps to New_Item
 573
 574             and Element (Container, Position) = New_Item
 575
 576             --  Other elements are preserved
 577
 578             and Model (Container)'Old <= Model (Container)
 579             and M.Included_Except
 580                   (Model (Container),
 581                    Model (Container)'Old,
 582                    New_Item)
 583
 584             --  The elements of Container located before Position are preserved
 585
 586             and E.Range_Equal
 587                   (Left  => Elements (Container)'Old,
 588                    Right => Elements (Container),
 589                    Fst   => 1,
 590                    Lst   => P.Get (Positions (Container), Position) - 1)
 591
 592             --  Other elements are shifted by 1
 593
 594             and E.Range_Shifted
 595                   (Left   => Elements (Container)'Old,
 596                    Right  => Elements (Container),
 597                    Fst    => P.Get (Positions (Container), Position),
 598                    Lst    => Length (Container)'Old,
 599                    Offset => 1)
 600
 601             --  A new cursor has been inserted at position Position in
 602             --  Container.
 603
 604             and P_Positions_Shifted
 605                   (Positions (Container)'Old,
 606                    Positions (Container),
 607                    Cut => P.Get (Positions (Container), Position)));
 608
 609    procedure Insert
 610      (Container : in out Set;
 611       New_Item  : Element_Type)
 612    with
 613      Global => null,
 614      Pre    =>
 615        Length (Container) < Container.Capacity
 616          and then (not Contains (Container, New_Item)),
 617      Post   =>
 618        Length (Container) = Length (Container)'Old + 1
 619          and Contains (Container, New_Item)
 620
 621          --  New_Item is inserted in the set
 622
 623          and E.Get (Elements (Container),
 624                     Find (Elements (Container), New_Item)) = New_Item
 625
 626          --  Other mappings are preserved
 627
 628          and Model (Container)'Old <= Model (Container)
 629          and M.Included_Except
 630                (Model (Container),
 631                 Model (Container)'Old,
 632                 New_Item)
 633
 634          --  The elements of Container located before New_Item are preserved
 635
 636          and E.Range_Equal
 637                (Left  => Elements (Container)'Old,
 638                 Right => Elements (Container),
 639                 Fst   => 1,
 640                 Lst   => Find (Elements (Container), New_Item) - 1)
 641
 642          --  Other elements are shifted by 1
 643
 644          and E.Range_Shifted
 645                (Left   => Elements (Container)'Old,
 646                 Right  => Elements (Container),
 647                 Fst    => Find (Elements (Container), New_Item),
 648                 Lst    => Length (Container)'Old,
 649                 Offset => 1)
 650
 651          --  A new cursor has been inserted in Container
 652
 653          and P_Positions_Shifted
 654                (Positions (Container)'Old,
 655                 Positions (Container),
 656                 Cut => Find (Elements (Container), New_Item));
 657
 658    procedure Include
 659      (Container : in out Set;
 660       New_Item  : Element_Type)
 661    with
 662      Global         => null,
 663      Pre            =>
 664        Length (Container) < Container.Capacity
 665          or Contains (Container, New_Item),
 666      Post           => Contains (Container, New_Item),
 667      Contract_Cases =>
 668
 669        --  If New_Item is already in Container
 670
 671        (Contains (Container, New_Item) =>
 672
 673           --  Elements are preserved
 674
 675           Model (Container)'Old = Model (Container)
 676
 677             --  Cursors are preserved
 678
 679             and Positions (Container) = Positions (Container)'Old
 680
 681             --  The element equivalent to New_Item in Container is replaced by
 682             --  New_Item.
 683
 684             and E.Get (Elements (Container),
 685                        Find (Elements (Container), New_Item)) = New_Item
 686
 687             and E.Equal_Except
 688                   (Elements (Container)'Old,
 689                    Elements (Container),
 690                    Find (Elements (Container), New_Item)),
 691
 692         --  Otherwise, New_Item is inserted in Container
 693
 694         others =>
 695           Length (Container) = Length (Container)'Old + 1
 696
 697             --  Other elements are preserved
 698
 699             and Model (Container)'Old <= Model (Container)
 700             and M.Included_Except
 701                   (Model (Container),
 702                    Model (Container)'Old,
 703                    New_Item)
 704
 705             --  New_Item is inserted in Container
 706
 707             and E.Get (Elements (Container),
 708                        Find (Elements (Container), New_Item)) = New_Item
 709
 710             --  The Elements of Container located before New_Item are preserved
 711
 712             and E.Range_Equal
 713                   (Left  => Elements (Container)'Old,
 714                    Right => Elements (Container),
 715                    Fst   => 1,
 716                    Lst   => Find (Elements (Container), New_Item) - 1)
 717
 718             --  Other Elements are shifted by 1
 719
 720             and E.Range_Shifted
 721                   (Left   => Elements (Container)'Old,
 722                    Right  => Elements (Container),
 723                    Fst    => Find (Elements (Container), New_Item),
 724                    Lst    => Length (Container)'Old,
 725                    Offset => 1)
 726
 727             --  A new cursor has been inserted in Container
 728
 729             and P_Positions_Shifted
 730                   (Positions (Container)'Old,
 731                    Positions (Container),
 732                    Cut => Find (Elements (Container), New_Item)));
 733
 734    procedure Replace
 735      (Container : in out Set;
 736       New_Item  : Element_Type)
 737    with
 738      Global => null,
 739      Pre    => Contains (Container, New_Item),
 740      Post   =>
 741
 742        --  Elements are preserved
 743
 744        Model (Container)'Old = Model (Container)
 745
 746          --  Cursors are preserved
 747
 748          and Positions (Container) = Positions (Container)'Old
 749
 750          --  The element equivalent to New_Item in Container is replaced by
 751          --  New_Item.
 752
 753          and E.Get (Elements (Container),
 754                     Find (Elements (Container), New_Item)) = New_Item
 755          and E.Equal_Except
 756               (Elements (Container)'Old,
 757                Elements (Container),
 758                Find (Elements (Container), New_Item));
 759
 760    procedure Exclude
 761      (Container : in out Set;
 762       Item      : Element_Type)
 763    with
 764      Global         => null,
 765      Post           => not Contains (Container, Item),
 766      Contract_Cases =>
 767
 768        --  If Item is not in Container, nothing is changed
 769
 770        (not Contains (Container, Item) =>
 771           Model (Container) = Model (Container)'Old
 772             and Elements (Container) = Elements (Container)'Old
 773             and Positions (Container) = Positions (Container)'Old,
 774
 775         --  Otherwise, Item is removed from Container
 776
 777         others =>
 778           Length (Container) = Length (Container)'Old - 1
 779
 780             --  Other elements are preserved
 781
 782             and Model (Container) <= Model (Container)'Old
 783             and M.Included_Except
 784                   (Model (Container)'Old,
 785                    Model (Container),
 786                    Item)
 787
 788             --  The elements of Container located before Item are preserved
 789
 790             and E.Range_Equal
 791                   (Left  => Elements (Container)'Old,
 792                    Right => Elements (Container),
 793                    Fst   => 1,
 794                    Lst   => Find (Elements (Container), Item)'Old - 1)
 795
 796             --  The elements located after Item are shifted by 1
 797
 798             and E.Range_Shifted
 799                   (Left   => Elements (Container),
 800                    Right  => Elements (Container)'Old,
 801                    Fst    => Find (Elements (Container), Item)'Old,
 802                    Lst    => Length (Container),
 803                    Offset => 1)
 804
 805             --  A cursor has been removed from Container
 806
 807             and P_Positions_Shifted
 808                   (Positions (Container),
 809                    Positions (Container)'Old,
 810                    Cut   => Find (Elements (Container), Item)'Old));
 811
 812    procedure Delete
 813      (Container : in out Set;
 814       Item      : Element_Type)
 815    with
 816      Global => null,
 817      Pre    => Contains (Container, Item),
 818      Post   =>
 819        Length (Container) = Length (Container)'Old - 1
 820
 821          --  Item is no longer in Container
 822
 823          and not Contains (Container, Item)
 824
 825          --  Other elements are preserved
 826
 827          and Model (Container) <= Model (Container)'Old
 828          and M.Included_Except
 829                (Model (Container)'Old,
 830                 Model (Container),
 831                 Item)
 832
 833          --  The elements of Container located before Item are preserved
 834
 835          and E.Range_Equal
 836                (Left  => Elements (Container)'Old,
 837                 Right => Elements (Container),
 838                 Fst   => 1,
 839                 Lst   => Find (Elements (Container), Item)'Old - 1)
 840
 841          --  The elements located after Item are shifted by 1
 842
 843          and E.Range_Shifted
 844                (Left   => Elements (Container),
 845                 Right  => Elements (Container)'Old,
 846                 Fst    => Find (Elements (Container), Item)'Old,
 847                 Lst    => Length (Container),
 848                 Offset => 1)
 849
 850          --  A cursor has been removed from Container
 851
 852          and P_Positions_Shifted
 853                (Positions (Container),
 854                 Positions (Container)'Old,
 855                 Cut   => Find (Elements (Container), Item)'Old);
 856
 857    procedure Delete
 858      (Container : in out Set;
 859       Position  : in out Cursor)
 860    with
 861      Global => null,
 862      Pre    => Has_Element (Container, Position),
 863      Post   =>
 864        Position = No_Element
 865          and Length (Container) = Length (Container)'Old - 1
 866
 867          --  The element at position Position is no longer in Container
 868
 869          and not Contains (Container, Element (Container, Position)'Old)
 870          and not P.Has_Key (Positions (Container), Position'Old)
 871
 872          --  Other elements are preserved
 873
 874          and Model (Container) <= Model (Container)'Old
 875          and M.Included_Except
 876                (Model (Container)'Old,
 877                 Model (Container),
 878                 Element (Container, Position)'Old)
 879
 880          --  The elements of Container located before Position are preserved.
 881
 882          and E.Range_Equal
 883                (Left  => Elements (Container)'Old,
 884                 Right => Elements (Container),
 885                 Fst   => 1,
 886                 Lst   => P.Get (Positions (Container)'Old, Position'Old) - 1)
 887
 888          --  The elements located after Position are shifted by 1
 889
 890          and E.Range_Shifted
 891                (Left   => Elements (Container),
 892                 Right  => Elements (Container)'Old,
 893                 Fst    => P.Get (Positions (Container)'Old, Position'Old),
 894                 Lst    => Length (Container),
 895                 Offset => 1)
 896
 897          --  Position has been removed from Container
 898
 899          and P_Positions_Shifted
 900                (Positions (Container),
 901                 Positions (Container)'Old,
 902                 Cut   => P.Get (Positions (Container)'Old, Position'Old));
 903
 904    procedure Delete_First (Container : in out Set) with
 905      Global         => null,
 906      Contract_Cases =>
 907        (Length (Container) = 0 => Length (Container) = 0,
 908         others =>
 909           Length (Container) = Length (Container)'Old - 1
 910
 911             --  The first element has been removed from Container
 912
 913             and not Contains (Container, First_Element (Container)'Old)
 914
 915             --  Other elements are preserved
 916
 917             and Model (Container) <= Model (Container)'Old
 918             and M.Included_Except
 919                   (Model (Container)'Old,
 920                    Model (Container),
 921                    First_Element (Container)'Old)
 922
 923             --  Other elements are shifted by 1
 924
 925             and E.Range_Shifted
 926                   (Left   => Elements (Container),
 927                    Right  => Elements (Container)'Old,
 928                    Fst    => 1,
 929                    Lst    => Length (Container),
 930                    Offset => 1)
 931
 932             --  First has been removed from Container
 933
 934             and P_Positions_Shifted
 935                   (Positions (Container),
 936                    Positions (Container)'Old,
 937                    Cut   => 1));
 938
 939    procedure Delete_Last (Container : in out Set) with
 940      Global         => null,
 941      Contract_Cases =>
 942        (Length (Container) = 0 => Length (Container) = 0,
 943         others =>
 944           Length (Container) = Length (Container)'Old - 1
 945
 946             --  The last element has been removed from Container
 947
 948             and not Contains (Container, Last_Element (Container)'Old)
 949
 950             --  Other elements are preserved
 951
 952             and Model (Container) <= Model (Container)'Old
 953             and M.Included_Except
 954                   (Model (Container)'Old,
 955                    Model (Container),
 956                    Last_Element (Container)'Old)
 957
 958             --  Others elements of Container are preserved
 959
 960             and E.Range_Equal
 961                   (Left  => Elements (Container)'Old,
 962                    Right => Elements (Container),
 963                    Fst   => 1,
 964                    Lst   => Length (Container))
 965
 966             --  Last cursor has been removed from Container
 967
 968             and Positions (Container) <= Positions (Container)'Old);
 969
 970    procedure Union (Target : in out Set; Source : Set) with
 971      Global => null,
 972      Pre    =>
 973        Length (Source) - Length (Target and Source) <=
 974          Target.Capacity - Length (Target),
 975      Post   =>
 976        Length (Target) = Length (Target)'Old
 977          - M.Num_Overlaps (Model (Target)'Old, Model (Source))
 978          + Length (Source)
 979
 980          --  Elements already in Target are still in Target
 981
 982          and Model (Target)'Old <= Model (Target)
 983
 984          --  Elements of Source are included in Target
 985
 986          and Model (Source) <= Model (Target)
 987
 988          --  Elements of Target come from either Source or Target
 989
 990          and
 991            M.Included_In_Union
 992              (Model (Target), Model (Source), Model (Target)'Old)
 993
 994          --  Actual value of elements come from either Left or Right
 995
 996          and
 997            E_Elements_Included
 998              (Elements (Target),
 999               Model (Target)'Old,
1000               Elements (Target)'Old,
1001               Elements (Source))
1002          and
1003            E_Elements_Included
1004              (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
1005          and
1006            E_Elements_Included
1007              (Elements (Source),
1008               Model (Target)'Old,
1009               Elements (Source),
1010               Elements (Target))
1011
1012          --  Mapping from cursors of Target to elements is preserved
1013
1014          and Mapping_Preserved
1015                (E_Left  => Elements (Target)'Old,
1016                 E_Right => Elements (Target),
1017                 P_Left  => Positions (Target)'Old,
1018                 P_Right => Positions (Target));
1019
1020    function Union (Left, Right : Set) return Set with
1021      Global => null,
1022      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
1023      Post   =>
1024        Length (Union'Result) = Length (Left)
1025          - M.Num_Overlaps (Model (Left), Model (Right))
1026          + Length (Right)
1027
1028          --  Elements of Left and Right are in the result of Union
1029
1030          and Model (Left) <= Model (Union'Result)
1031          and Model (Right) <= Model (Union'Result)
1032
1033          --  Elements of the result of union come from either Left or Right
1034
1035          and
1036            M.Included_In_Union
1037              (Model (Union'Result), Model (Left), Model (Right))
1038
1039          --  Actual value of elements come from either Left or Right
1040
1041          and
1042            E_Elements_Included
1043              (Elements (Union'Result),
1044               Model (Left),
1045               Elements (Left),
1046               Elements (Right))
1047          and
1048            E_Elements_Included
1049              (Elements (Left), Model (Left), Elements (Union'Result))
1050          and
1051            E_Elements_Included
1052              (Elements (Right),
1053               Model (Left),
1054               Elements (Right),
1055               Elements (Union'Result));
1056
1057    function "or" (Left, Right : Set) return Set renames Union;
1058
1059    procedure Intersection (Target : in out Set; Source : Set) with
1060      Global => null,
1061      Post   =>
1062        Length (Target) =
1063          M.Num_Overlaps (Model (Target)'Old, Model (Source))
1064
1065          --  Elements of Target were already in Target
1066
1067          and Model (Target) <= Model (Target)'Old
1068
1069          --  Elements of Target are in Source
1070
1071          and Model (Target) <= Model (Source)
1072
1073          --  Elements both in Source and Target are in the intersection
1074
1075          and
1076            M.Includes_Intersection
1077              (Model (Target), Model (Source), Model (Target)'Old)
1078
1079          --  Actual value of elements of Target is preserved
1080
1081          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1082          and
1083            E_Elements_Included
1084              (Elements (Target)'Old, Model (Source), Elements (Target))
1085
1086          --  Mapping from cursors of Target to elements is preserved
1087
1088          and Mapping_Preserved
1089                (E_Left  => Elements (Target),
1090                 E_Right => Elements (Target)'Old,
1091                 P_Left  => Positions (Target),
1092                 P_Right => Positions (Target)'Old);
1093
1094    function Intersection (Left, Right : Set) return Set with
1095      Global => null,
1096      Post   =>
1097        Length (Intersection'Result) =
1098          M.Num_Overlaps (Model (Left), Model (Right))
1099
1100          --  Elements in the result of Intersection are in Left and Right
1101
1102          and Model (Intersection'Result) <= Model (Left)
1103          and Model (Intersection'Result) <= Model (Right)
1104
1105          --  Elements both in Left and Right are in the result of Intersection
1106
1107          and
1108            M.Includes_Intersection
1109              (Model (Intersection'Result), Model (Left), Model (Right))
1110
1111          --  Actual value of elements come from Left
1112
1113          and
1114            E_Elements_Included
1115              (Elements (Intersection'Result), Elements (Left))
1116          and
1117            E_Elements_Included
1118              (Elements (Left), Model (Right), Elements (Intersection'Result));
1119
1120    function "and" (Left, Right : Set) return Set renames Intersection;
1121
1122    procedure Difference (Target : in out Set; Source : Set) with
1123      Global => null,
1124      Post   =>
1125        Length (Target) = Length (Target)'Old -
1126          M.Num_Overlaps (Model (Target)'Old, Model (Source))
1127
1128          --  Elements of Target were already in Target
1129
1130          and Model (Target) <= Model (Target)'Old
1131
1132          --  Elements of Target are not in Source
1133
1134          and M.No_Overlap (Model (Target), Model (Source))
1135
1136          --  Elements in Target but not in Source are in the difference
1137
1138          and
1139            M.Included_In_Union
1140              (Model (Target)'Old, Model (Target), Model (Source))
1141
1142          --  Actual value of elements of Target is preserved
1143
1144          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1145          and
1146            E_Elements_Included
1147              (Elements (Target)'Old, Model (Target), Elements (Target))
1148
1149          --  Mapping from cursors of Target to elements is preserved
1150
1151          and Mapping_Preserved
1152                (E_Left  => Elements (Target),
1153                 E_Right => Elements (Target)'Old,
1154                 P_Left  => Positions (Target),
1155                 P_Right => Positions (Target)'Old);
1156
1157    function Difference (Left, Right : Set) return Set with
1158      Global => null,
1159      Post   =>
1160        Length (Difference'Result) = Length (Left) -
1161          M.Num_Overlaps (Model (Left), Model (Right))
1162
1163          --  Elements of the result of Difference are in Left
1164
1165          and Model (Difference'Result) <= Model (Left)
1166
1167          --  Elements of the result of Difference are in Right
1168
1169          and M.No_Overlap (Model (Difference'Result), Model (Right))
1170
1171          --  Elements in Left but not in Right are in the difference
1172
1173          and
1174            M.Included_In_Union
1175              (Model (Left), Model (Difference'Result), Model (Right))
1176
1177          --  Actual value of elements come from Left
1178
1179          and
1180            E_Elements_Included (Elements (Difference'Result), Elements (Left))
1181          and
1182            E_Elements_Included
1183              (Elements (Left),
1184               Model (Difference'Result),
1185               Elements (Difference'Result));
1186
1187    function "-" (Left, Right : Set) return Set renames Difference;
1188
1189    procedure Symmetric_Difference (Target : in out Set; Source : Set) with
1190      Global => null,
1191      Pre    =>
1192        Length (Source) - Length (Target and Source) <=
1193          Target.Capacity - Length (Target) + Length (Target and Source),
1194      Post   =>
1195        Length (Target) = Length (Target)'Old -
1196          2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
1197          Length (Source)
1198
1199          --  Elements of the difference were not both in Source and in Target
1200
1201          and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
1202
1203          --  Elements in Target but not in Source are in the difference
1204
1205          and
1206            M.Included_In_Union
1207              (Model (Target)'Old, Model (Target), Model (Source))
1208
1209          --  Elements in Source but not in Target are in the difference
1210
1211          and
1212            M.Included_In_Union
1213              (Model (Source), Model (Target), Model (Target)'Old)
1214
1215          --  Actual value of elements come from either Left or Right
1216
1217          and
1218            E_Elements_Included
1219              (Elements (Target),
1220               Model (Target)'Old,
1221               Elements (Target)'Old,
1222               Elements (Source))
1223          and
1224            E_Elements_Included
1225              (Elements (Target)'Old, Model (Target), Elements (Target))
1226          and
1227            E_Elements_Included
1228              (Elements (Source), Model (Target), Elements (Target));
1229
1230    function Symmetric_Difference (Left, Right : Set) return Set with
1231      Global => null,
1232      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
1233      Post   =>
1234        Length (Symmetric_Difference'Result) = Length (Left) -
1235          2 * M.Num_Overlaps (Model (Left), Model (Right)) +
1236          Length (Right)
1237
1238          --  Elements of the difference were not both in Left and Right
1239
1240          and
1241            M.Not_In_Both
1242              (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
1243
1244          --  Elements in Left but not in Right are in the difference
1245
1246          and
1247            M.Included_In_Union
1248              (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
1249
1250          --  Elements in Right but not in Left are in the difference
1251
1252          and
1253            M.Included_In_Union
1254              (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
1255
1256          --  Actual value of elements come from either Left or Right
1257
1258          and
1259            E_Elements_Included
1260              (Elements (Symmetric_Difference'Result),
1261               Model (Left),
1262               Elements (Left),
1263               Elements (Right))
1264          and
1265            E_Elements_Included
1266              (Elements (Left),
1267               Model (Symmetric_Difference'Result),
1268               Elements (Symmetric_Difference'Result))
1269          and
1270            E_Elements_Included
1271              (Elements (Right),
1272               Model (Symmetric_Difference'Result),
1273               Elements (Symmetric_Difference'Result));
1274
1275    function "xor" (Left, Right : Set) return Set
1276      renames Symmetric_Difference;
1277
1278    function Overlap (Left, Right : Set) return Boolean with
1279      Global => null,
1280      Post   =>
1281        Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
1282
1283    function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
1284      Global => null,
1285      Post   => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
1286
1287    function First (Container : Set) return Cursor with
1288      Global         => null,
1289      Contract_Cases =>
1290        (Length (Container) = 0 =>
1291           First'Result = No_Element,
1292
1293         others =>
1294           Has_Element (Container, First'Result)
1295             and P.Get (Positions (Container), First'Result) = 1);
1296
1297    function First_Element (Container : Set) return Element_Type with
1298      Global => null,
1299      Pre    => not Is_Empty (Container),
1300      Post   =>
1301        First_Element'Result = E.Get (Elements (Container), 1)
1302          and E_Smaller_Than_Range
1303                (Elements (Container),
1304                 2,
1305                 Length (Container),
1306                 First_Element'Result);
1307
1308    function Last (Container : Set) return Cursor with
1309      Global         => null,
1310      Contract_Cases =>
1311        (Length (Container) = 0 =>
1312           Last'Result = No_Element,
1313
1314         others =>
1315           Has_Element (Container, Last'Result)
1316             and P.Get (Positions (Container), Last'Result) =
1317                   Length (Container));
1318
1319    function Last_Element (Container : Set) return Element_Type with
1320      Global => null,
1321      Pre    => not Is_Empty (Container),
1322      Post   =>
1323        Last_Element'Result = E.Get (Elements (Container), Length (Container))
1324          and E_Bigger_Than_Range
1325                (Elements (Container),
1326                 1,
1327                 Length (Container) - 1,
1328                 Last_Element'Result);
1329
1330    function Next (Container : Set; Position : Cursor) return Cursor with
1331      Global         => null,
1332      Pre            =>
1333        Has_Element (Container, Position) or else Position = No_Element,
1334      Contract_Cases =>
1335        (Position = No_Element
1336           or else P.Get (Positions (Container), Position) = Length (Container)
1337         =>
1338           Next'Result = No_Element,
1339
1340         others =>
1341           Has_Element (Container, Next'Result)
1342             and then P.Get (Positions (Container), Next'Result) =
1343                      P.Get (Positions (Container), Position) + 1);
1344
1345    procedure Next (Container : Set; Position : in out Cursor) with
1346      Global         => null,
1347      Pre            =>
1348        Has_Element (Container, Position) or else Position = No_Element,
1349      Contract_Cases =>
1350        (Position = No_Element
1351           or else P.Get (Positions (Container), Position) = Length (Container)
1352         =>
1353           Position = No_Element,
1354
1355         others =>
1356           Has_Element (Container, Position)
1357             and then P.Get (Positions (Container), Position) =
1358                      P.Get (Positions (Container), Position'Old) + 1);
1359
1360    function Previous (Container : Set; Position : Cursor) return Cursor with
1361      Global         => null,
1362      Pre            =>
1363        Has_Element (Container, Position) or else Position = No_Element,
1364      Contract_Cases =>
1365        (Position = No_Element
1366           or else P.Get (Positions (Container), Position) = 1
1367         =>
1368           Previous'Result = No_Element,
1369
1370         others =>
1371           Has_Element (Container, Previous'Result)
1372             and then P.Get (Positions (Container), Previous'Result) =
1373                      P.Get (Positions (Container), Position) - 1);
1374
1375    procedure Previous (Container : Set; Position : in out Cursor) with
1376      Global         => null,
1377      Pre            =>
1378        Has_Element (Container, Position) or else Position = No_Element,
1379      Contract_Cases =>
1380        (Position = No_Element
1381           or else P.Get (Positions (Container), Position) = 1
1382          =>
1383           Position = No_Element,
1384
1385         others =>
1386           Has_Element (Container, Position)
1387             and then P.Get (Positions (Container), Position) =
1388                      P.Get (Positions (Container), Position'Old) - 1);
1389
1390    function Find (Container : Set; Item : Element_Type) return Cursor with
1391      Global         => null,
1392      Contract_Cases =>
1393
1394        --  If Item is not contained in Container, Find returns No_Element
1395
1396        (not Contains (Model (Container), Item) =>
1397           not P.Has_Key (Positions (Container), Find'Result)
1398             and Find'Result = No_Element,
1399
1400         --  Otherwise, Find returns a valid cursor in Container
1401
1402         others =>
1403           P.Has_Key (Positions (Container), Find'Result)
1404             and P.Get (Positions (Container), Find'Result) =
1405                 Find (Elements (Container), Item)
1406
1407             --  The element designated by the result of Find is Item
1408
1409             and Equivalent_Elements
1410                   (Element (Container, Find'Result), Item));
1411
1412    function Floor (Container : Set; Item : Element_Type) return Cursor with
1413      Global         => null,
1414      Contract_Cases =>
1415        (Length (Container) = 0 or else Item < First_Element (Container) =>
1416           Floor'Result = No_Element,
1417         others =>
1418           Has_Element (Container, Floor'Result)
1419             and
1420               not (Item < E.Get (Elements (Container),
1421                                  P.Get (Positions (Container), Floor'Result)))
1422             and E_Is_Find
1423                   (Elements (Container),
1424                    Item,
1425                    P.Get (Positions (Container), Floor'Result)));
1426
1427    function Ceiling (Container : Set; Item : Element_Type) return Cursor with
1428      Global         => null,
1429      Contract_Cases =>
1430        (Length (Container) = 0 or else Last_Element (Container) < Item =>
1431           Ceiling'Result = No_Element,
1432         others =>
1433           Has_Element (Container, Ceiling'Result)
1434             and
1435               not (E.Get (Elements (Container),
1436                           P.Get (Positions (Container), Ceiling'Result)) <
1437                    Item)
1438             and E_Is_Find
1439                   (Elements (Container),
1440                    Item,
1441                    P.Get (Positions (Container), Ceiling'Result)));
1442
1443    function Contains (Container : Set; Item : Element_Type) return Boolean with
1444      Global => null,
1445      Post   => Contains'Result = Contains (Model (Container), Item);
1446    pragma Annotate (GNATprove, Inline_For_Proof, Contains);
1447
1448    function Has_Element (Container : Set; Position : Cursor) return Boolean
1449    with
1450      Global => null,
1451      Post   =>
1452        Has_Element'Result = P.Has_Key (Positions (Container), Position);
1453    pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
1454
1455    generic
1456       type Key_Type (<>) is private;
1457
1458       with function Key (Element : Element_Type) return Key_Type;
1459
1460       with function "<" (Left, Right : Key_Type) return Boolean is <>;
1461
1462    package Generic_Keys with SPARK_Mode is
1463
1464       function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
1465         Global => null,
1466         Post   =>
1467           Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left));
1468       pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys);
1469
1470       package Formal_Model with Ghost is
1471          function E_Bigger_Than_Range
1472            (Container : E.Sequence;
1473             Fst       : Positive_Count_Type;
1474             Lst       : Count_Type;
1475             Key       : Key_Type) return Boolean
1476          with
1477            Global => null,
1478            Pre    => Lst <= E.Length (Container),
1479            Post   =>
1480              E_Bigger_Than_Range'Result =
1481                (for all I in Fst .. Lst =>
1482                   Generic_Keys.Key (E.Get (Container, I)) < Key);
1483          pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
1484
1485          function E_Smaller_Than_Range
1486            (Container : E.Sequence;
1487             Fst       : Positive_Count_Type;
1488             Lst       : Count_Type;
1489             Key       : Key_Type) return Boolean
1490          with
1491            Global => null,
1492            Pre    => Lst <= E.Length (Container),
1493            Post   =>
1494              E_Smaller_Than_Range'Result =
1495                (for all I in Fst .. Lst =>
1496                   Key < Generic_Keys.Key (E.Get (Container, I)));
1497          pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
1498
1499          function E_Is_Find
1500            (Container : E.Sequence;
1501             Key       : Key_Type;
1502             Position  : Count_Type) return Boolean
1503          with
1504            Global => null,
1505            Pre    => Position - 1 <= E.Length (Container),
1506            Post   =>
1507              E_Is_Find'Result =
1508
1509                ((if Position > 0 then
1510                    E_Bigger_Than_Range (Container, 1, Position - 1, Key))
1511
1512                      and (if Position < E.Length (Container) then
1513                         E_Smaller_Than_Range
1514                           (Container,
1515                            Position + 1,
1516                            E.Length (Container),
1517                            Key)));
1518          pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
1519
1520          function Find
1521            (Container : E.Sequence;
1522             Key       : Key_Type) return Count_Type
1523          --  Search for Key in Container
1524
1525            with
1526              Global                  => null,
1527              Post                    =>
1528                (if Find'Result > 0 then
1529                   Find'Result <= E.Length (Container)
1530                     and Equivalent_Keys
1531                       (Key, Generic_Keys.Key (E.Get (Container, Find'Result)))
1532                     and E_Is_Find (Container, Key, Find'Result));
1533
1534          function M_Included_Except
1535            (Left  : M.Set;
1536             Right : M.Set;
1537             Key   : Key_Type) return Boolean
1538            with
1539              Global                  => null,
1540              Post                    =>
1541                M_Included_Except'Result =
1542                  (for all E of Left =>
1543                     Contains (Right, E)
1544                       or Equivalent_Keys (Generic_Keys.Key (E), Key));
1545       end Formal_Model;
1546       use Formal_Model;
1547
1548       function Key (Container : Set; Position : Cursor) return Key_Type with
1549         Global => null,
1550         Post   => Key'Result = Key (Element (Container, Position));
1551       pragma Annotate (GNATprove, Inline_For_Proof, Key);
1552
1553       function Element (Container : Set; Key : Key_Type) return Element_Type
1554       with
1555         Global => null,
1556         Pre    => Contains (Container, Key),
1557         Post   =>
1558           Element'Result = Element (Container, Find (Container, Key));
1559       pragma Annotate (GNATprove, Inline_For_Proof, Element);
1560
1561       procedure Replace
1562         (Container : in out Set;
1563          Key       : Key_Type;
1564          New_Item  : Element_Type)
1565       with
1566         Global => null,
1567         Pre    => Contains (Container, Key),
1568         Post   =>
1569           Length (Container) = Length (Container)'Old
1570
1571              --  Key now maps to New_Item
1572
1573              and Element (Container, Key) = New_Item
1574
1575              --  New_Item is contained in Container
1576
1577              and Contains (Model (Container), New_Item)
1578
1579              --  Other elements are preserved
1580
1581              and M_Included_Except
1582                    (Model (Container)'Old,
1583                     Model (Container),
1584                     Key)
1585              and M.Included_Except
1586                    (Model (Container),
1587                     Model (Container)'Old,
1588                     New_Item)
1589
1590              --  Mapping from cursors to elements is preserved
1591
1592              and Mapping_Preserved_Except
1593                    (E_Left   => Elements (Container)'Old,
1594                     E_Right  => Elements (Container),
1595                     P_Left   => Positions (Container)'Old,
1596                     P_Right  => Positions (Container),
1597                     Position => Find (Container, Key))
1598              and Positions (Container) = Positions (Container)'Old;
1599
1600       procedure Exclude (Container : in out Set; Key : Key_Type) with
1601         Global         => null,
1602         Post           => not Contains (Container, Key),
1603         Contract_Cases =>
1604
1605           --  If Key is not in Container, nothing is changed
1606
1607           (not Contains (Container, Key) =>
1608              Model (Container) = Model (Container)'Old
1609                and Elements (Container) = Elements (Container)'Old
1610                and Positions (Container) = Positions (Container)'Old,
1611
1612            --  Otherwise, Key is removed from Container
1613
1614            others =>
1615              Length (Container) = Length (Container)'Old - 1
1616
1617                --  Other elements are preserved
1618
1619                and Model (Container) <= Model (Container)'Old
1620                and M_Included_Except
1621                      (Model (Container)'Old,
1622                       Model (Container),
1623                       Key)
1624
1625                --  The elements of Container located before Key are preserved
1626
1627                and E.Range_Equal
1628                      (Left  => Elements (Container)'Old,
1629                       Right => Elements (Container),
1630                       Fst   => 1,
1631                       Lst   => Find (Elements (Container), Key)'Old - 1)
1632
1633                --  The elements located after Key are shifted by 1
1634
1635                and E.Range_Shifted
1636                      (Left   => Elements (Container),
1637                       Right  => Elements (Container)'Old,
1638                       Fst    => Find (Elements (Container), Key)'Old,
1639                       Lst    => Length (Container),
1640                       Offset => 1)
1641
1642                --  A cursor has been removed from Container
1643
1644                and P_Positions_Shifted
1645                      (Positions (Container),
1646                       Positions (Container)'Old,
1647                       Cut   => Find (Elements (Container), Key)'Old));
1648
1649       procedure Delete (Container : in out Set; Key : Key_Type) with
1650         Global => null,
1651         Pre    => Contains (Container, Key),
1652         Post   =>
1653           Length (Container) = Length (Container)'Old - 1
1654
1655             --  Key is no longer in Container
1656
1657             and not Contains (Container, Key)
1658
1659             --  Other elements are preserved
1660
1661             and Model (Container) <= Model (Container)'Old
1662             and M_Included_Except
1663                   (Model (Container)'Old,
1664                    Model (Container),
1665                    Key)
1666
1667             --  The elements of Container located before Key are preserved
1668
1669             and E.Range_Equal
1670                   (Left  => Elements (Container)'Old,
1671                    Right => Elements (Container),
1672                    Fst   => 1,
1673                    Lst   => Find (Elements (Container), Key)'Old - 1)
1674
1675             --  The elements located after Key are shifted by 1
1676
1677             and E.Range_Shifted
1678                   (Left   => Elements (Container),
1679                    Right  => Elements (Container)'Old,
1680                    Fst    => Find (Elements (Container), Key)'Old,
1681                    Lst    => Length (Container),
1682                    Offset => 1)
1683
1684             --  A cursor has been removed from Container
1685
1686             and P_Positions_Shifted
1687                   (Positions (Container),
1688                    Positions (Container)'Old,
1689                    Cut   => Find (Elements (Container), Key)'Old);
1690
1691       function Find (Container : Set; Key : Key_Type) return Cursor with
1692         Global         => null,
1693         Contract_Cases =>
1694
1695           --  If Key is not contained in Container, Find returns No_Element
1696
1697           ((for all E of Model (Container) =>
1698                not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
1699              not P.Has_Key (Positions (Container), Find'Result)
1700                and Find'Result = No_Element,
1701
1702            --  Otherwise, Find returns a valid cursor in Container
1703
1704            others =>
1705              P.Has_Key (Positions (Container), Find'Result)
1706                and P.Get (Positions (Container), Find'Result) =
1707                    Find (Elements (Container), Key)
1708
1709                --  The element designated by the result of Find is Key
1710
1711                and Equivalent_Keys
1712                   (Generic_Keys.Key (Element (Container, Find'Result)), Key));
1713
1714       function Floor (Container : Set; Key : Key_Type) return Cursor with
1715         Global         => null,
1716         Contract_Cases =>
1717           (Length (Container) = 0
1718              or else Key < Generic_Keys.Key (First_Element (Container)) =>
1719              Floor'Result = No_Element,
1720            others =>
1721               Has_Element (Container, Floor'Result)
1722                and
1723                  not (Key <
1724                       Generic_Keys.Key
1725                        (E.Get (Elements (Container),
1726                                P.Get (Positions (Container), Floor'Result))))
1727                and E_Is_Find
1728                      (Elements (Container),
1729                       Key,
1730                       P.Get (Positions (Container), Floor'Result)));
1731
1732       function Ceiling (Container : Set; Key : Key_Type) return Cursor with
1733         Global         => null,
1734         Contract_Cases =>
1735           (Length (Container) = 0
1736              or else Generic_Keys.Key (Last_Element (Container)) < Key =>
1737              Ceiling'Result = No_Element,
1738            others =>
1739              Has_Element (Container, Ceiling'Result)
1740                and
1741                  not (Generic_Keys.Key
1742                        (E.Get (Elements (Container),
1743                                P.Get (Positions (Container), Ceiling'Result)))
1744                       < Key)
1745                and E_Is_Find
1746                      (Elements (Container),
1747                       Key,
1748                       P.Get (Positions (Container), Ceiling'Result)));
1749
1750       function Contains (Container : Set; Key : Key_Type) return Boolean with
1751         Global => null,
1752         Post   =>
1753           Contains'Result =
1754             (for some E of Model (Container) =>
1755                 Equivalent_Keys (Key, Generic_Keys.Key (E)));
1756
1757    end Generic_Keys;
1758
1759 private
1760    pragma SPARK_Mode (Off);
1761
1762    pragma Inline (Next);
1763    pragma Inline (Previous);
1764
1765    type Node_Type is record
1766       Has_Element : Boolean := False;
1767       Parent  : Count_Type := 0;
1768       Left    : Count_Type := 0;
1769       Right   : Count_Type := 0;
1770       Color   : Red_Black_Trees.Color_Type;
1771       Element : Element_Type;
1772    end record;
1773
1774    package Tree_Types is
1775      new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
1776
1777    type Set (Capacity : Count_Type) is
1778      new Tree_Types.Tree_Type (Capacity) with null record;
1779
1780    use Red_Black_Trees;
1781
1782    Empty_Set : constant Set := (Capacity => 0, others => <>);
1783
1784 end Ada.Containers.Formal_Ordered_Sets;