gcc/ada/a-cfhase.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 _ H A S H 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_Hashed_Sets in the
  33 --  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: Element, Next, Query_Element, Has_Element, Key,
  42 --    Iterate, Equivalent_Elements. This change is motivated by the need to
  43 --    have cursors which are valid on different containers (typically a
  44 --    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.
  47
  48 with Ada.Containers.Functional_Maps;
  49 with Ada.Containers.Functional_Sets;
  50 with Ada.Containers.Functional_Vectors;
  51 private with Ada.Containers.Hash_Tables;
  52
  53 generic
  54    type Element_Type is private;
  55
  56    with function Hash (Element : Element_Type) return Hash_Type;
  57
  58    with function Equivalent_Elements
  59      (Left  : Element_Type;
  60       Right : Element_Type) return Boolean is "=";
  61
  62 package Ada.Containers.Formal_Hashed_Sets with
  63   SPARK_Mode
  64 is
  65    pragma Annotate (CodePeer, Skip_Analysis);
  66
  67    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
  68      Iterable => (First       => First,
  69                   Next        => Next,
  70                   Has_Element => Has_Element,
  71                   Element     => Element),
  72      Default_Initial_Condition => Is_Empty (Set);
  73    pragma Preelaborable_Initialization (Set);
  74
  75    type Cursor is record
  76       Node : Count_Type;
  77    end record;
  78
  79    No_Element : constant Cursor := (Node => 0);
  80
  81    function Length (Container : Set) return Count_Type with
  82      Global => null,
  83      Post   => Length'Result <= Container.Capacity;
  84
  85    pragma Unevaluated_Use_Of_Old (Allow);
  86
  87    package Formal_Model with Ghost is
  88       subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
  89
  90       package M is new Ada.Containers.Functional_Sets
  91         (Element_Type    => Element_Type,
  92          Equivalent_Elements => Equivalent_Elements);
  93
  94       function "="
  95         (Left  : M.Set;
  96          Right : M.Set) return Boolean renames M."=";
  97
  98       function "<="
  99         (Left  : M.Set;
 100          Right : M.Set) return Boolean renames M."<=";
 101
 102       package E is new Ada.Containers.Functional_Vectors
 103         (Element_Type => Element_Type,
 104          Index_Type   => Positive_Count_Type);
 105
 106       function "="
 107         (Left  : E.Sequence;
 108          Right : E.Sequence) return Boolean renames E."=";
 109
 110       function "<"
 111         (Left  : E.Sequence;
 112          Right : E.Sequence) return Boolean renames E."<";
 113
 114       function "<="
 115         (Left  : E.Sequence;
 116          Right : E.Sequence) return Boolean renames E."<=";
 117
 118       function Find
 119         (Container : E.Sequence;
 120          Item      : Element_Type) return Count_Type
 121       --  Search for Item in Container
 122
 123       with
 124         Global => null,
 125         Post =>
 126           (if Find'Result > 0 then
 127               Find'Result <= E.Length (Container)
 128                 and Equivalent_Elements
 129                       (Item, E.Get (Container, Find'Result)));
 130
 131       function E_Elements_Included
 132         (Left  : E.Sequence;
 133          Right : E.Sequence) return Boolean
 134       --  The elements of Left are contained in Right
 135
 136       with
 137         Global => null,
 138         Post   =>
 139           E_Elements_Included'Result =
 140             (for all I in 1 .. E.Length (Left) =>
 141               Find (Right, E.Get (Left, I)) > 0
 142                 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
 143                          E.Get (Left, I));
 144       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 145
 146       function E_Elements_Included
 147         (Left  : E.Sequence;
 148          Model : M.Set;
 149          Right : E.Sequence) return Boolean
 150       --  The elements of Container contained in Model are in Right
 151
 152       with
 153         Global => null,
 154         Post   =>
 155           E_Elements_Included'Result =
 156             (for all I in 1 .. E.Length (Left) =>
 157               (if M.Contains (Model, E.Get (Left, I)) then
 158                   Find (Right, E.Get (Left, I)) > 0
 159                     and then E.Get (Right, Find (Right, E.Get (Left, I))) =
 160                              E.Get (Left, I)));
 161       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 162
 163       function E_Elements_Included
 164         (Container : E.Sequence;
 165          Model     : M.Set;
 166          Left      : E.Sequence;
 167          Right     : E.Sequence) return Boolean
 168       --  The elements of Container contained in Model are in Left and others
 169       --  are in Right.
 170
 171       with
 172         Global => null,
 173         Post   =>
 174           E_Elements_Included'Result =
 175             (for all I in 1 .. E.Length (Container) =>
 176               (if M.Contains (Model, E.Get (Container, I)) then
 177                   Find (Left, E.Get (Container, I)) > 0
 178                     and then E.Get (Left, Find (Left, E.Get (Container, I))) =
 179                              E.Get (Container, I)
 180                else
 181                   Find (Right, E.Get (Container, I)) > 0
 182                     and then E.Get
 183                                (Right, Find (Right, E.Get (Container, I))) =
 184                              E.Get (Container, I)));
 185       pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
 186
 187       package P is new Ada.Containers.Functional_Maps
 188         (Key_Type                       => Cursor,
 189          Element_Type                   => Positive_Count_Type,
 190          Equivalent_Keys                => "=",
 191          Enable_Handling_Of_Equivalence => False);
 192
 193       function "="
 194         (Left  : P.Map;
 195          Right : P.Map) return Boolean renames P."=";
 196
 197       function "<="
 198         (Left  : P.Map;
 199          Right : P.Map) return Boolean renames P."<=";
 200
 201       function Mapping_Preserved
 202         (E_Left  : E.Sequence;
 203          E_Right : E.Sequence;
 204          P_Left  : P.Map;
 205          P_Right : P.Map) return Boolean
 206       with
 207         Ghost,
 208         Global => null,
 209         Post   =>
 210           (if Mapping_Preserved'Result then
 211
 212              --  Right contains all the cursors of Left
 213
 214              P.Keys_Included (P_Left, P_Right)
 215
 216                --  Right contains all the elements of Left
 217
 218                and E_Elements_Included (E_Left, E_Right)
 219
 220                --  Mappings from cursors to elements induced by E_Left, P_Left
 221                --  and E_Right, P_Right are the same.
 222
 223                and (for all C of P_Left =>
 224                      E.Get (E_Left, P.Get (P_Left, C)) =
 225                      E.Get (E_Right, P.Get (P_Right, C))));
 226
 227       function Mapping_Preserved_Except
 228         (E_Left   : E.Sequence;
 229          E_Right  : E.Sequence;
 230          P_Left   : P.Map;
 231          P_Right  : P.Map;
 232          Position : Cursor) return Boolean
 233       with
 234         Ghost,
 235         Global => null,
 236         Post   =>
 237           (if Mapping_Preserved_Except'Result then
 238
 239              --  Right contains all the cursors of Left
 240
 241              P.Keys_Included (P_Left, P_Right)
 242
 243                --  Mappings from cursors to elements induced by E_Left, P_Left
 244                --  and E_Right, P_Right are the same except for Position.
 245
 246                and (for all C of P_Left =>
 247                      (if C /= Position then
 248                          E.Get (E_Left, P.Get (P_Left, C)) =
 249                          E.Get (E_Right, P.Get (P_Right, C)))));
 250
 251       function Model (Container : Set) return M.Set with
 252       --  The high-level model of a set is a set of elements. Neither cursors
 253       --  nor order of elements are represented in this model. Elements are
 254       --  modeled up to equivalence.
 255
 256         Ghost,
 257         Global => null,
 258         Post   => M.Length (Model'Result) = Length (Container);
 259
 260       function Elements (Container : Set) return E.Sequence with
 261       --  The Elements sequence represents the underlying list structure of
 262       --  sets that is used for iteration. It stores the actual values of
 263       --  elements in the set. It does not model cursors.
 264
 265         Ghost,
 266         Global => null,
 267         Post   =>
 268           E.Length (Elements'Result) = Length (Container)
 269
 270             --  It only contains keys contained in Model
 271
 272             and (for all Item of Elements'Result =>
 273                   M.Contains (Model (Container), Item))
 274
 275             --  It contains all the elements contained in Model
 276
 277             and (for all Item of Model (Container) =>
 278                   (Find (Elements'Result, Item) > 0
 279                     and then Equivalent_Elements
 280                                (E.Get (Elements'Result,
 281                                        Find (Elements'Result, Item)),
 282                                 Item)))
 283
 284             --  It has no duplicate
 285
 286             and (for all I in 1 .. Length (Container) =>
 287                   Find (Elements'Result, E.Get (Elements'Result, I)) = I)
 288
 289             and (for all I in 1 .. Length (Container) =>
 290                   (for all J in 1 .. Length (Container) =>
 291                     (if Equivalent_Elements
 292                           (E.Get (Elements'Result, I),
 293                            E.Get (Elements'Result, J))
 294                      then I = J)));
 295       pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
 296
 297       function Positions (Container : Set) return P.Map with
 298       --  The Positions map is used to model cursors. It only contains valid
 299       --  cursors and maps them to their position in the container.
 300
 301         Ghost,
 302         Global => null,
 303         Post   =>
 304           not P.Has_Key (Positions'Result, No_Element)
 305
 306             --  Positions of cursors are smaller than the container's length
 307
 308             and then
 309               (for all I of Positions'Result =>
 310                 P.Get (Positions'Result, I) in 1 .. Length (Container)
 311
 312             --  No two cursors have the same position. Note that we do not
 313             --  state that there is a cursor in the map for each position, as
 314             --  it is rarely needed.
 315
 316             and then
 317               (for all J of Positions'Result =>
 318                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
 319                  then I = J)));
 320
 321       procedure Lift_Abstraction_Level (Container : Set) with
 322         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
 323         --  assume that we can access the same elements by iterating over
 324         --  positions or cursors.
 325         --  This information is not generally useful except when switching from
 326         --  a low-level, cursor-aware view of a container, to a high-level,
 327         --  position-based view.
 328
 329         Ghost,
 330         Global => null,
 331         Post   =>
 332           (for all Item of Elements (Container) =>
 333             (for some I of Positions (Container) =>
 334               E.Get (Elements (Container), P.Get (Positions (Container), I)) =
 335                 Item));
 336
 337       function Contains
 338         (C : M.Set;
 339          K : Element_Type) return Boolean renames M.Contains;
 340       --  To improve readability of contracts, we rename the function used to
 341       --  search for an element in the model to Contains.
 342
 343    end Formal_Model;
 344    use Formal_Model;
 345
 346    Empty_Set : constant Set;
 347
 348    function "=" (Left, Right : Set) return Boolean with
 349      Global => null,
 350      Post   =>
 351          "="'Result =
 352            (Length (Left) = Length (Right)
 353              and E_Elements_Included (Elements (Left), Elements (Right)))
 354        and
 355          "="'Result =
 356            (E_Elements_Included (Elements (Left), Elements (Right))
 357              and E_Elements_Included (Elements (Right), Elements (Left)));
 358
 359    function Equivalent_Sets (Left, Right : Set) return Boolean with
 360      Global => null,
 361      Post   => Equivalent_Sets'Result = (Model (Left) = Model (Right));
 362
 363    function To_Set (New_Item : Element_Type) return Set with
 364      Global => null,
 365      Post   =>
 366        M.Is_Singleton (Model (To_Set'Result), New_Item)
 367          and Length (To_Set'Result) = 1
 368          and E.Get (Elements (To_Set'Result), 1) = New_Item;
 369
 370    function Capacity (Container : Set) return Count_Type with
 371      Global => null,
 372      Post   => Capacity'Result = Container.Capacity;
 373
 374    procedure Reserve_Capacity
 375      (Container : in out Set;
 376       Capacity  : Count_Type)
 377    with
 378      Global => null,
 379      Pre    => Capacity <= Container.Capacity,
 380      Post   =>
 381        Model (Container) = Model (Container)'Old
 382          and Length (Container)'Old = Length (Container)
 383
 384          --  Actual elements are preserved
 385
 386          and E_Elements_Included
 387               (Elements (Container), Elements (Container)'Old)
 388          and E_Elements_Included
 389               (Elements (Container)'Old, Elements (Container));
 390
 391    function Is_Empty (Container : Set) return Boolean with
 392      Global => null,
 393      Post   => Is_Empty'Result = (Length (Container) = 0);
 394
 395    procedure Clear (Container : in out Set) with
 396      Global => null,
 397      Post   => Length (Container) = 0 and M.Is_Empty (Model (Container));
 398
 399    procedure Assign (Target : in out Set; Source : Set) with
 400      Global => null,
 401      Pre    => Target.Capacity >= Length (Source),
 402      Post   =>
 403        Model (Target) = Model (Source)
 404          and Length (Target) = Length (Source)
 405
 406          --  Actual elements are preserved
 407
 408          and E_Elements_Included (Elements (Target), Elements (Source))
 409          and E_Elements_Included (Elements (Source), Elements (Target));
 410
 411    function Copy
 412      (Source   : Set;
 413       Capacity : Count_Type := 0) return Set
 414    with
 415      Global => null,
 416      Pre    => Capacity = 0 or else Capacity >= Source.Capacity,
 417      Post   =>
 418        Model (Copy'Result) = Model (Source)
 419          and Elements (Copy'Result) = Elements (Source)
 420          and Positions (Copy'Result) = Positions (Source)
 421          and (if Capacity = 0 then
 422                  Copy'Result.Capacity = Source.Capacity
 423               else
 424                  Copy'Result.Capacity = Capacity);
 425
 426    function Element
 427      (Container : Set;
 428       Position  : Cursor) return Element_Type
 429    with
 430      Global => null,
 431      Pre    => Has_Element (Container, Position),
 432      Post   =>
 433        Element'Result =
 434          E.Get (Elements (Container), P.Get (Positions (Container), Position));
 435    pragma Annotate (GNATprove, Inline_For_Proof, Element);
 436
 437    procedure Replace_Element
 438      (Container : in out Set;
 439       Position  : Cursor;
 440       New_Item  : Element_Type)
 441    with
 442      Global => null,
 443      Pre    => Has_Element (Container, Position),
 444      Post   =>
 445        Length (Container) = Length (Container)'Old
 446
 447           --  Position now maps to New_Item
 448
 449           and Element (Container, Position) = New_Item
 450
 451           --  New_Item is contained in Container
 452
 453           and Contains (Model (Container), New_Item)
 454
 455           --  Other elements are preserved
 456
 457           and M.Included_Except
 458                 (Model (Container)'Old,
 459                  Model (Container),
 460                  Element (Container, Position)'Old)
 461           and M.Included_Except
 462                 (Model (Container),
 463                  Model (Container)'Old,
 464                  New_Item)
 465
 466           --  Mapping from cursors to elements is preserved
 467
 468           and Mapping_Preserved_Except
 469                 (E_Left   => Elements (Container)'Old,
 470                  E_Right  => Elements (Container),
 471                  P_Left   => Positions (Container)'Old,
 472                  P_Right  => Positions (Container),
 473                  Position => Position)
 474           and Positions (Container) = Positions (Container)'Old;
 475
 476    procedure Move (Target : in out Set; Source : in out Set) with
 477      Global => null,
 478      Pre    => Target.Capacity >= Length (Source),
 479      Post   =>
 480        Length (Source) = 0
 481          and Model (Target) = Model (Source)'Old
 482          and Length (Target) = Length (Source)'Old
 483
 484          --  Actual elements are preserved
 485
 486          and E_Elements_Included (Elements (Target), Elements (Source)'Old)
 487          and E_Elements_Included (Elements (Source)'Old, Elements (Target));
 488
 489    procedure Insert
 490      (Container : in out Set;
 491       New_Item  : Element_Type;
 492       Position  : out Cursor;
 493       Inserted  : out Boolean)
 494    with
 495      Global         => null,
 496      Pre            =>
 497        Length (Container) < Container.Capacity
 498          or Contains (Container, New_Item),
 499      Post           =>
 500        Contains (Container, New_Item)
 501          and Has_Element (Container, Position)
 502          and Equivalent_Elements (Element (Container, Position), New_Item),
 503      Contract_Cases =>
 504
 505        --  If New_Item is already in Container, it is not modified and Inserted
 506        --  is set to False.
 507
 508        (Contains (Container, New_Item) =>
 509           not Inserted
 510             and Model (Container) = Model (Container)'Old
 511             and Elements (Container) = Elements (Container)'Old
 512             and Positions (Container) = Positions (Container)'Old,
 513
 514         --  Otherwise, New_Item is inserted in Container and Inserted is set to
 515         --  True.
 516
 517         others =>
 518           Inserted
 519             and Length (Container) = Length (Container)'Old + 1
 520
 521             --  Position now maps to New_Item
 522
 523             and Element (Container, Position) = New_Item
 524
 525             --  Other elements are preserved
 526
 527             and Model (Container)'Old <= Model (Container)
 528             and M.Included_Except
 529                   (Model (Container),
 530                    Model (Container)'Old,
 531                    New_Item)
 532
 533             --  Mapping from cursors to elements is preserved
 534
 535             and Mapping_Preserved
 536                   (E_Left  => Elements (Container)'Old,
 537                    E_Right => Elements (Container),
 538                    P_Left  => Positions (Container)'Old,
 539                    P_Right => Positions (Container))
 540             and P.Keys_Included_Except
 541                   (Positions (Container),
 542                    Positions (Container)'Old,
 543                    Position));
 544
 545    procedure Insert  (Container : in out Set; New_Item : Element_Type) with
 546      Global => null,
 547      Pre    => Length (Container) < Container.Capacity
 548                  and then (not Contains (Container, New_Item)),
 549      Post   =>
 550        Length (Container) = Length (Container)'Old + 1
 551          and Contains (Container, New_Item)
 552          and Element (Container, Find (Container, New_Item)) = New_Item
 553
 554          --  Other elements are preserved
 555
 556          and Model (Container)'Old <= Model (Container)
 557          and M.Included_Except
 558                (Model (Container),
 559                 Model (Container)'Old,
 560                 New_Item)
 561
 562          --  Mapping from cursors to elements is preserved
 563
 564          and Mapping_Preserved
 565                (E_Left  => Elements (Container)'Old,
 566                 E_Right => Elements (Container),
 567                 P_Left  => Positions (Container)'Old,
 568                 P_Right => Positions (Container))
 569          and P.Keys_Included_Except
 570                (Positions (Container),
 571                 Positions (Container)'Old,
 572                 Find (Container, New_Item));
 573
 574    procedure Include (Container : in out Set; New_Item : Element_Type) with
 575      Global         => null,
 576      Pre            =>
 577        Length (Container) < Container.Capacity
 578          or Contains (Container, New_Item),
 579      Post           =>
 580        Contains (Container, New_Item)
 581          and Element (Container, Find (Container, New_Item)) = New_Item,
 582      Contract_Cases =>
 583
 584        --  If an element equivalent to New_Item is already in Container, it is
 585        --  replaced by New_Item.
 586
 587        (Contains (Container, New_Item) =>
 588
 589           --  Elements are preserved modulo equivalence
 590
 591           Model (Container) = Model (Container)'Old
 592
 593             --  Cursors are preserved
 594
 595             and Positions (Container) = Positions (Container)'Old
 596
 597             --  The actual value of other elements is preserved
 598
 599             and E.Equal_Except
 600                   (Elements (Container)'Old,
 601                    Elements (Container),
 602                    P.Get (Positions (Container), Find (Container, New_Item))),
 603
 604         --  Otherwise, New_Item is inserted in Container
 605
 606         others =>
 607           Length (Container) = Length (Container)'Old + 1
 608
 609             --  Other elements are preserved
 610
 611             and Model (Container)'Old <= Model (Container)
 612             and M.Included_Except
 613                   (Model (Container),
 614                    Model (Container)'Old,
 615                    New_Item)
 616
 617             --  Mapping from cursors to elements is preserved
 618
 619             and Mapping_Preserved
 620                   (E_Left  => Elements (Container)'Old,
 621                    E_Right => Elements (Container),
 622                    P_Left  => Positions (Container)'Old,
 623                    P_Right => Positions (Container))
 624             and P.Keys_Included_Except
 625                   (Positions (Container),
 626                    Positions (Container)'Old,
 627                    Find (Container, New_Item)));
 628
 629    procedure Replace (Container : in out Set; New_Item : Element_Type) with
 630      Global => null,
 631      Pre    => Contains (Container, New_Item),
 632      Post   =>
 633
 634        --  Elements are preserved modulo equivalence
 635
 636        Model (Container) = Model (Container)'Old
 637          and Contains (Container, New_Item)
 638
 639          --  Cursors are preserved
 640
 641          and Positions (Container) = Positions (Container)'Old
 642
 643          --  The element equivalent to New_Item in Container is replaced by
 644          --  New_Item.
 645
 646          and Element (Container, Find (Container, New_Item)) = New_Item
 647          and E.Equal_Except
 648                (Elements (Container)'Old,
 649                 Elements (Container),
 650                 P.Get (Positions (Container), Find (Container, New_Item)));
 651
 652    procedure Exclude (Container : in out Set; Item : Element_Type) with
 653      Global         => null,
 654      Post           => not Contains (Container, Item),
 655      Contract_Cases =>
 656
 657        --  If Item is not in Container, nothing is changed
 658
 659        (not Contains (Container, Item) =>
 660           Model (Container) = Model (Container)'Old
 661             and Elements (Container) = Elements (Container)'Old
 662             and Positions (Container) = Positions (Container)'Old,
 663
 664         --  Otherwise, Item is removed from Container
 665
 666         others =>
 667           Length (Container) = Length (Container)'Old - 1
 668
 669             --  Other elements are preserved
 670
 671             and Model (Container) <= Model (Container)'Old
 672             and M.Included_Except
 673                   (Model (Container)'Old,
 674                    Model (Container),
 675                    Item)
 676
 677             --  Mapping from cursors to elements is preserved
 678
 679             and Mapping_Preserved
 680                   (E_Left  => Elements (Container),
 681                    E_Right => Elements (Container)'Old,
 682                    P_Left  => Positions (Container),
 683                    P_Right => Positions (Container)'Old)
 684             and P.Keys_Included_Except
 685                   (Positions (Container)'Old,
 686                    Positions (Container),
 687                    Find (Container, Item)'Old));
 688
 689    procedure Delete  (Container : in out Set; Item : Element_Type) with
 690      Global => null,
 691      Pre    => Contains (Container, Item),
 692      Post   =>
 693        Length (Container) = Length (Container)'Old - 1
 694
 695          --  Item is no longer in Container
 696
 697          and not Contains (Container, Item)
 698
 699          --  Other elements are preserved
 700
 701          and Model (Container) <= Model (Container)'Old
 702          and M.Included_Except
 703                (Model (Container)'Old,
 704                 Model (Container),
 705                 Item)
 706
 707          --  Mapping from cursors to elements is preserved
 708
 709          and Mapping_Preserved
 710                (E_Left  => Elements (Container),
 711                 E_Right => Elements (Container)'Old,
 712                 P_Left  => Positions (Container),
 713                 P_Right => Positions (Container)'Old)
 714          and P.Keys_Included_Except
 715                (Positions (Container)'Old,
 716                 Positions (Container),
 717                 Find (Container, Item)'Old);
 718
 719    procedure Delete (Container : in out Set; Position : in out Cursor) with
 720      Global => null,
 721      Pre    => Has_Element (Container, Position),
 722      Post   =>
 723        Position = No_Element
 724          and Length (Container) = Length (Container)'Old - 1
 725
 726          --  The element at position Position is no longer in Container
 727
 728          and not Contains (Container, Element (Container, Position)'Old)
 729          and not P.Has_Key (Positions (Container), Position'Old)
 730
 731          --  Other elements are preserved
 732
 733          and Model (Container) <= Model (Container)'Old
 734          and M.Included_Except
 735                (Model (Container)'Old,
 736                 Model (Container),
 737                 Element (Container, Position)'Old)
 738
 739          --  Mapping from cursors to elements is preserved
 740
 741          and Mapping_Preserved
 742                (E_Left  => Elements (Container),
 743                 E_Right => Elements (Container)'Old,
 744                 P_Left  => Positions (Container),
 745                 P_Right => Positions (Container)'Old)
 746          and P.Keys_Included_Except
 747                (Positions (Container)'Old,
 748                 Positions (Container),
 749                 Position'Old);
 750
 751    procedure Union (Target : in out Set; Source : Set) with
 752      Global => null,
 753      Pre    =>
 754        Length (Source) - Length (Target and Source) <=
 755          Target.Capacity - Length (Target),
 756      Post   =>
 757        Length (Target) = Length (Target)'Old
 758          - M.Num_Overlaps (Model (Target)'Old, Model (Source))
 759          + Length (Source)
 760
 761          --  Elements already in Target are still in Target
 762
 763          and Model (Target)'Old <= Model (Target)
 764
 765          --  Elements of Source are included in Target
 766
 767          and Model (Source) <= Model (Target)
 768
 769          --  Elements of Target come from either Source or Target
 770
 771          and M.Included_In_Union
 772                (Model (Target), Model (Source), Model (Target)'Old)
 773
 774          --  Actual value of elements come from either Left or Right
 775
 776          and E_Elements_Included
 777                (Elements (Target),
 778                 Model (Target)'Old,
 779                 Elements (Target)'Old,
 780                 Elements (Source))
 781
 782          and E_Elements_Included
 783                (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
 784
 785          and E_Elements_Included
 786                (Elements (Source),
 787                 Model (Target)'Old,
 788                 Elements (Source),
 789                 Elements (Target))
 790
 791          --  Mapping from cursors of Target to elements is preserved
 792
 793          and Mapping_Preserved
 794                (E_Left  => Elements (Target)'Old,
 795                 E_Right => Elements (Target),
 796                 P_Left  => Positions (Target)'Old,
 797                 P_Right => Positions (Target));
 798
 799    function Union (Left, Right : Set) return Set with
 800      Global => null,
 801      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
 802      Post   =>
 803        Length (Union'Result) = Length (Left)
 804          - M.Num_Overlaps (Model (Left), Model (Right))
 805          + Length (Right)
 806
 807          --  Elements of Left and Right are in the result of Union
 808
 809          and Model (Left) <= Model (Union'Result)
 810          and Model (Right) <= Model (Union'Result)
 811
 812          --  Elements of the result of union come from either Left or Right
 813
 814          and
 815            M.Included_In_Union
 816              (Model (Union'Result), Model (Left), Model (Right))
 817
 818          --  Actual value of elements come from either Left or Right
 819
 820          and E_Elements_Included
 821                (Elements (Union'Result),
 822                 Model (Left),
 823                 Elements (Left),
 824                 Elements (Right))
 825
 826          and E_Elements_Included
 827                (Elements (Left), Model (Left), Elements (Union'Result))
 828
 829          and E_Elements_Included
 830                (Elements (Right),
 831                 Model (Left),
 832                 Elements (Right),
 833                 Elements (Union'Result));
 834
 835    function "or" (Left, Right : Set) return Set renames Union;
 836
 837    procedure Intersection (Target : in out Set; Source : Set) with
 838      Global => null,
 839      Post   =>
 840        Length (Target) =
 841          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 842
 843          --  Elements of Target were already in Target
 844
 845          and Model (Target) <= Model (Target)'Old
 846
 847          --  Elements of Target are in Source
 848
 849          and Model (Target) <= Model (Source)
 850
 851          --  Elements both in Source and Target are in the intersection
 852
 853          and M.Includes_Intersection
 854                (Model (Target), Model (Source), Model (Target)'Old)
 855
 856          --  Actual value of elements of Target is preserved
 857
 858          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
 859          and E_Elements_Included
 860                (Elements (Target)'Old, Model (Source), Elements (Target))
 861
 862          --  Mapping from cursors of Target to elements is preserved
 863
 864          and Mapping_Preserved
 865                (E_Left  => Elements (Target),
 866                 E_Right => Elements (Target)'Old,
 867                 P_Left  => Positions (Target),
 868                 P_Right => Positions (Target)'Old);
 869
 870    function Intersection (Left, Right : Set) return Set with
 871      Global => null,
 872      Post   =>
 873        Length (Intersection'Result) =
 874          M.Num_Overlaps (Model (Left), Model (Right))
 875
 876          --  Elements in the result of Intersection are in Left and Right
 877
 878          and Model (Intersection'Result) <= Model (Left)
 879          and Model (Intersection'Result) <= Model (Right)
 880
 881          --  Elements both in Left and Right are in the result of Intersection
 882
 883          and M.Includes_Intersection
 884                (Model (Intersection'Result), Model (Left), Model (Right))
 885
 886          --  Actual value of elements come from Left
 887
 888          and E_Elements_Included
 889                (Elements (Intersection'Result), Elements (Left))
 890
 891          and E_Elements_Included
 892                (Elements (Left), Model (Right),
 893                 Elements (Intersection'Result));
 894
 895    function "and" (Left, Right : Set) return Set renames Intersection;
 896
 897    procedure Difference (Target : in out Set; Source : Set) with
 898      Global => null,
 899      Post   =>
 900        Length (Target) = Length (Target)'Old -
 901          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 902
 903          --  Elements of Target were already in Target
 904
 905          and Model (Target) <= Model (Target)'Old
 906
 907          --  Elements of Target are not in Source
 908
 909          and M.No_Overlap (Model (Target), Model (Source))
 910
 911          --  Elements in Target but not in Source are in the difference
 912
 913          and M.Included_In_Union
 914                (Model (Target)'Old, Model (Target), Model (Source))
 915
 916          --  Actual value of elements of Target is preserved
 917
 918          and E_Elements_Included (Elements (Target), Elements (Target)'Old)
 919          and E_Elements_Included
 920                (Elements (Target)'Old, Model (Target), Elements (Target))
 921
 922          --  Mapping from cursors of Target to elements is preserved
 923
 924          and Mapping_Preserved
 925                (E_Left  => Elements (Target),
 926                 E_Right => Elements (Target)'Old,
 927                 P_Left  => Positions (Target),
 928                 P_Right => Positions (Target)'Old);
 929
 930    function Difference (Left, Right : Set) return Set with
 931      Global => null,
 932      Post   =>
 933        Length (Difference'Result) = Length (Left) -
 934          M.Num_Overlaps (Model (Left), Model (Right))
 935
 936          --  Elements of the result of Difference are in Left
 937
 938          and Model (Difference'Result) <= Model (Left)
 939
 940          --  Elements of the result of Difference are in Right
 941
 942          and M.No_Overlap (Model (Difference'Result), Model (Right))
 943
 944          --  Elements in Left but not in Right are in the difference
 945
 946          and M.Included_In_Union
 947                (Model (Left), Model (Difference'Result), Model (Right))
 948
 949          --  Actual value of elements come from Left
 950
 951          and E_Elements_Included
 952                (Elements (Difference'Result), Elements (Left))
 953
 954          and E_Elements_Included
 955                (Elements (Left),
 956                 Model (Difference'Result),
 957                 Elements (Difference'Result));
 958
 959    function "-" (Left, Right : Set) return Set renames Difference;
 960
 961    procedure Symmetric_Difference (Target : in out Set; Source : Set) with
 962      Global => null,
 963      Pre    =>
 964        Length (Source) - Length (Target and Source) <=
 965          Target.Capacity - Length (Target) + Length (Target and Source),
 966      Post   =>
 967        Length (Target) = Length (Target)'Old -
 968          2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
 969          Length (Source)
 970
 971          --  Elements of the difference were not both in Source and in Target
 972
 973          and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
 974
 975          --  Elements in Target but not in Source are in the difference
 976
 977          and M.Included_In_Union
 978                (Model (Target)'Old, Model (Target), Model (Source))
 979
 980          --  Elements in Source but not in Target are in the difference
 981
 982          and M.Included_In_Union
 983                (Model (Source), Model (Target), Model (Target)'Old)
 984
 985          --  Actual value of elements come from either Left or Right
 986
 987          and E_Elements_Included
 988                (Elements (Target),
 989                 Model (Target)'Old,
 990                 Elements (Target)'Old,
 991                 Elements (Source))
 992
 993          and E_Elements_Included
 994                (Elements (Target)'Old, Model (Target), Elements (Target))
 995
 996          and E_Elements_Included
 997                (Elements (Source), Model (Target), Elements (Target));
 998
 999    function Symmetric_Difference (Left, Right : Set) return Set with
1000      Global => null,
1001      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
1002      Post   =>
1003        Length (Symmetric_Difference'Result) = Length (Left) -
1004          2 * M.Num_Overlaps (Model (Left), Model (Right)) +
1005          Length (Right)
1006
1007          --  Elements of the difference were not both in Left and Right
1008
1009          and M.Not_In_Both
1010                (Model (Symmetric_Difference'Result),
1011                 Model (Left),
1012                 Model (Right))
1013
1014          --  Elements in Left but not in Right are in the difference
1015
1016          and M.Included_In_Union
1017                (Model (Left),
1018                 Model (Symmetric_Difference'Result),
1019                 Model (Right))
1020
1021          --  Elements in Right but not in Left are in the difference
1022
1023          and M.Included_In_Union
1024                (Model (Right),
1025                 Model (Symmetric_Difference'Result),
1026                 Model (Left))
1027
1028          --  Actual value of elements come from either Left or Right
1029
1030          and E_Elements_Included
1031                (Elements (Symmetric_Difference'Result),
1032                 Model (Left),
1033                 Elements (Left),
1034                 Elements (Right))
1035
1036          and E_Elements_Included
1037                (Elements (Left),
1038                 Model (Symmetric_Difference'Result),
1039                 Elements (Symmetric_Difference'Result))
1040
1041          and E_Elements_Included
1042                (Elements (Right),
1043                 Model (Symmetric_Difference'Result),
1044                 Elements (Symmetric_Difference'Result));
1045
1046    function "xor" (Left, Right : Set) return Set
1047      renames Symmetric_Difference;
1048
1049    function Overlap (Left, Right : Set) return Boolean with
1050      Global => null,
1051      Post   =>
1052        Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
1053
1054    function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
1055      Global => null,
1056      Post   => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
1057
1058    function First (Container : Set) return Cursor with
1059      Global         => null,
1060      Contract_Cases =>
1061        (Length (Container) = 0 =>
1062           First'Result = No_Element,
1063
1064         others =>
1065           Has_Element (Container, First'Result)
1066             and P.Get (Positions (Container), First'Result) = 1);
1067
1068    function Next (Container : Set; Position : Cursor) return Cursor with
1069      Global         => null,
1070      Pre            =>
1071        Has_Element (Container, Position) or else Position = No_Element,
1072      Contract_Cases =>
1073        (Position = No_Element
1074           or else P.Get (Positions (Container), Position) = Length (Container)
1075         =>
1076           Next'Result = No_Element,
1077
1078         others =>
1079           Has_Element (Container, Next'Result)
1080             and then P.Get (Positions (Container), Next'Result) =
1081                      P.Get (Positions (Container), Position) + 1);
1082
1083    procedure Next (Container : Set; Position : in out Cursor) with
1084      Global         => null,
1085      Pre            =>
1086        Has_Element (Container, Position) or else Position = No_Element,
1087      Contract_Cases =>
1088        (Position = No_Element
1089           or else P.Get (Positions (Container), Position) = Length (Container)
1090         =>
1091           Position = No_Element,
1092
1093         others =>
1094           Has_Element (Container, Position)
1095             and then P.Get (Positions (Container), Position) =
1096                      P.Get (Positions (Container), Position'Old) + 1);
1097
1098    function Find
1099      (Container : Set;
1100       Item      : Element_Type) return Cursor
1101    with
1102      Global         => null,
1103      Contract_Cases =>
1104
1105        --  If Item is not contained in Container, Find returns No_Element
1106
1107        (not Contains (Model (Container), Item) =>
1108           Find'Result = No_Element,
1109
1110         --  Otherwise, Find returns a valid cursor in Container
1111
1112         others =>
1113           P.Has_Key (Positions (Container), Find'Result)
1114             and P.Get (Positions (Container), Find'Result) =
1115                 Find (Elements (Container), Item)
1116
1117             --  The element designated by the result of Find is Item
1118
1119             and Equivalent_Elements
1120                   (Element (Container, Find'Result), Item));
1121
1122    function Contains (Container : Set; Item : Element_Type) return Boolean with
1123      Global => null,
1124      Post   => Contains'Result = Contains (Model (Container), Item);
1125    pragma Annotate (GNATprove, Inline_For_Proof, Contains);
1126
1127    function Has_Element (Container : Set; Position : Cursor) return Boolean
1128    with
1129      Global => null,
1130      Post   =>
1131        Has_Element'Result = P.Has_Key (Positions (Container), Position);
1132    pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
1133
1134    function Default_Modulus (Capacity : Count_Type) return Hash_Type with
1135      Global => null;
1136
1137    generic
1138       type Key_Type (<>) is private;
1139
1140       with function Key (Element : Element_Type) return Key_Type;
1141
1142       with function Hash (Key : Key_Type) return Hash_Type;
1143
1144       with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
1145
1146    package Generic_Keys with SPARK_Mode is
1147
1148       package Formal_Model with Ghost is
1149
1150          function M_Included_Except
1151            (Left  : M.Set;
1152             Right : M.Set;
1153             Key   : Key_Type) return Boolean
1154            with
1155              Global => null,
1156              Post   =>
1157                M_Included_Except'Result =
1158                  (for all E of Left =>
1159                    Contains (Right, E)
1160                      or Equivalent_Keys (Generic_Keys.Key (E), Key));
1161
1162       end Formal_Model;
1163       use Formal_Model;
1164
1165       function Key (Container : Set; Position : Cursor) return Key_Type with
1166         Global => null,
1167         Post   => Key'Result = Key (Element (Container, Position));
1168       pragma Annotate (GNATprove, Inline_For_Proof, Key);
1169
1170       function Element (Container : Set; Key : Key_Type) return Element_Type
1171       with
1172         Global => null,
1173         Pre    => Contains (Container, Key),
1174         Post   =>
1175           Element'Result = Element (Container, Find (Container, Key));
1176       pragma Annotate (GNATprove, Inline_For_Proof, Element);
1177
1178       procedure Replace
1179         (Container : in out Set;
1180          Key       : Key_Type;
1181          New_Item  : Element_Type)
1182       with
1183         Global => null,
1184         Pre    => Contains (Container, Key),
1185         Post   =>
1186           Length (Container) = Length (Container)'Old
1187
1188              --  Key now maps to New_Item
1189
1190              and Element (Container, Key) = New_Item
1191
1192              --  New_Item is contained in Container
1193
1194              and Contains (Model (Container), New_Item)
1195
1196              --  Other elements are preserved
1197
1198              and M_Included_Except
1199                    (Model (Container)'Old,
1200                     Model (Container),
1201                     Key)
1202              and M.Included_Except
1203                    (Model (Container),
1204                     Model (Container)'Old,
1205                     New_Item)
1206
1207              --  Mapping from cursors to elements is preserved
1208
1209              and Mapping_Preserved_Except
1210                    (E_Left   => Elements (Container)'Old,
1211                     E_Right  => Elements (Container),
1212                     P_Left   => Positions (Container)'Old,
1213                     P_Right  => Positions (Container),
1214                     Position => Find (Container, Key))
1215              and Positions (Container) = Positions (Container)'Old;
1216
1217       procedure Exclude (Container : in out Set; Key : Key_Type) with
1218         Global         => null,
1219         Post           => not Contains (Container, Key),
1220         Contract_Cases =>
1221
1222           --  If Key is not in Container, nothing is changed
1223
1224           (not Contains (Container, Key) =>
1225              Model (Container) = Model (Container)'Old
1226                and Elements (Container) = Elements (Container)'Old
1227                and Positions (Container) = Positions (Container)'Old,
1228
1229            --  Otherwise, Key is removed from Container
1230
1231            others =>
1232              Length (Container) = Length (Container)'Old - 1
1233
1234                --  Other elements are preserved
1235
1236                and Model (Container) <= Model (Container)'Old
1237                and M_Included_Except
1238                      (Model (Container)'Old,
1239                       Model (Container),
1240                       Key)
1241
1242                --  Mapping from cursors to elements is preserved
1243
1244                and Mapping_Preserved
1245                      (E_Left  => Elements (Container),
1246                       E_Right => Elements (Container)'Old,
1247                       P_Left  => Positions (Container),
1248                       P_Right => Positions (Container)'Old)
1249                and P.Keys_Included_Except
1250                      (Positions (Container)'Old,
1251                       Positions (Container),
1252                       Find (Container, Key)'Old));
1253
1254       procedure Delete (Container : in out Set; Key : Key_Type) with
1255         Global => null,
1256         Pre    => Contains (Container, Key),
1257         Post   =>
1258           Length (Container) = Length (Container)'Old - 1
1259
1260             --  Key is no longer in Container
1261
1262             and not Contains (Container, Key)
1263
1264             --  Other elements are preserved
1265
1266             and Model (Container) <= Model (Container)'Old
1267             and M_Included_Except
1268                   (Model (Container)'Old,
1269                    Model (Container),
1270                    Key)
1271
1272             --  Mapping from cursors to elements is preserved
1273
1274             and Mapping_Preserved
1275                   (E_Left  => Elements (Container),
1276                    E_Right => Elements (Container)'Old,
1277                    P_Left  => Positions (Container),
1278                    P_Right => Positions (Container)'Old)
1279             and P.Keys_Included_Except
1280                   (Positions (Container)'Old,
1281                    Positions (Container),
1282                    Find (Container, Key)'Old);
1283
1284       function Find (Container : Set; Key : Key_Type) return Cursor with
1285         Global         => null,
1286         Contract_Cases =>
1287
1288           --  If Key is not contained in Container, Find returns No_Element
1289
1290           ((for all E of Model (Container) =>
1291                not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
1292              Find'Result = No_Element,
1293
1294            --  Otherwise, Find returns a valid cursor in Container
1295
1296            others =>
1297              P.Has_Key (Positions (Container), Find'Result)
1298
1299                --  The key designated by the result of Find is Key
1300
1301                and Equivalent_Keys
1302                      (Generic_Keys.Key (Container, Find'Result), Key));
1303
1304       function Contains (Container : Set; Key : Key_Type) return Boolean with
1305         Global => null,
1306         Post   =>
1307           Contains'Result =
1308             (for some E of Model (Container) =>
1309               Equivalent_Keys (Key, Generic_Keys.Key (E)));
1310
1311    end Generic_Keys;
1312
1313 private
1314    pragma SPARK_Mode (Off);
1315
1316    pragma Inline (Next);
1317
1318    type Node_Type is
1319       record
1320          Element     : Element_Type;
1321          Next        : Count_Type;
1322          Has_Element : Boolean := False;
1323       end record;
1324
1325    package HT_Types is new
1326      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
1327
1328    type Set (Capacity : Count_Type; Modulus : Hash_Type) is
1329      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
1330
1331    use HT_Types;
1332
1333    Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
1334
1335 end Ada.Containers.Formal_Hashed_Sets;