gcc/ada/a-cfhama.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 _ M A P 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_Maps 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 --    contents of a container: Key, Element, Next, Query_Element, Has_Element,
  42 --    Iterate, Equivalent_Keys. This change is motivated by the need to have
  43 --    cursors which are valid on different containers (typically a container C
  44 --    and its previous version C'Old) for expressing properties, which is not
  45 --    possible if cursors encapsulate an access to the underlying container.
  46
  47 --  Iteration over maps is done using the Iterable aspect, which is SPARK
  48 --  compatible. "For of" iteration ranges over keys instead of elements.
  49
  50 with Ada.Containers.Functional_Vectors;
  51 with Ada.Containers.Functional_Maps;
  52 private with Ada.Containers.Hash_Tables;
  53
  54 generic
  55    type Key_Type is private;
  56    type Element_Type is private;
  57
  58    with function Hash (Key : Key_Type) return Hash_Type;
  59    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
  60
  61 package Ada.Containers.Formal_Hashed_Maps with
  62   SPARK_Mode
  63 is
  64    pragma Annotate (CodePeer, Skip_Analysis);
  65
  66    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
  67      Iterable => (First       => First,
  68                   Next        => Next,
  69                   Has_Element => Has_Element,
  70                   Element     => Key),
  71      Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0;
  72    pragma Preelaborable_Initialization (Map);
  73
  74    Empty_Map : constant Map;
  75
  76    type Cursor is record
  77       Node : Count_Type;
  78    end record;
  79
  80    No_Element : constant Cursor := (Node => 0);
  81
  82    function Length (Container : Map) return Count_Type with
  83      Global => null,
  84      Post   => Length'Result <= Container.Capacity;
  85
  86    pragma Unevaluated_Use_Of_Old (Allow);
  87
  88    package Formal_Model with Ghost is
  89       subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
  90
  91       package M is new Ada.Containers.Functional_Maps
  92         (Element_Type    => Element_Type,
  93          Key_Type        => Key_Type,
  94          Equivalent_Keys => Equivalent_Keys);
  95
  96       function "="
  97         (Left  : M.Map;
  98          Right : M.Map) return Boolean renames M."=";
  99
 100       function "<="
 101         (Left  : M.Map;
 102          Right : M.Map) return Boolean renames M."<=";
 103
 104       package K is new Ada.Containers.Functional_Vectors
 105         (Element_Type => Key_Type,
 106          Index_Type   => Positive_Count_Type);
 107
 108       function "="
 109         (Left  : K.Sequence;
 110          Right : K.Sequence) return Boolean renames K."=";
 111
 112       function "<"
 113         (Left  : K.Sequence;
 114          Right : K.Sequence) return Boolean renames K."<";
 115
 116       function "<="
 117         (Left  : K.Sequence;
 118          Right : K.Sequence) return Boolean renames K."<=";
 119
 120       package P is new Ada.Containers.Functional_Maps
 121         (Key_Type        => Cursor,
 122          Element_Type    => Positive_Count_Type,
 123          Equivalent_Keys => "=");
 124
 125       function "="
 126         (Left  : P.Map;
 127          Right : P.Map) return Boolean renames P."=";
 128
 129       function "<="
 130         (Left  : P.Map;
 131          Right : P.Map) return Boolean renames P."<=";
 132
 133       function Mapping_Preserved
 134         (K_Left  : K.Sequence;
 135          K_Right : K.Sequence;
 136          P_Left  : P.Map;
 137          P_Right : P.Map) return Boolean
 138       with
 139         Ghost,
 140         Global => null,
 141         Post   =>
 142           (if Mapping_Preserved'Result then
 143
 144              --  Right contains all the cursors of Left
 145
 146              P.Keys_Included (P_Left, P_Right)
 147
 148                --  Mappings from cursors to elements induced by K_Left, P_Left
 149                --  and K_Right, P_Right are the same.
 150
 151                and (for all C of P_Left =>
 152                      K.Get (K_Left, P.Get (P_Left, C)) =
 153                      K.Get (K_Right, P.Get (P_Right, C))));
 154
 155       function Model (Container : Map) return M.Map with
 156       --  The high-level model of a map is a map from keys to elements. Neither
 157       --  cursors nor order of elements are represented in this model. Keys are
 158       --  modeled up to equivalence.
 159
 160         Ghost,
 161         Global => null;
 162
 163       function Keys (Container : Map) return K.Sequence with
 164       --  The Keys sequence represents the underlying list structure of maps
 165       --  that is used for iteration. It stores the actual values of keys in
 166       --  the map. It does not model cursors nor elements.
 167
 168         Ghost,
 169         Global => null,
 170         Post   =>
 171           K.Length (Keys'Result) = Length (Container)
 172
 173             --  It only contains keys contained in Model
 174
 175             and (for all Key of Keys'Result =>
 176                    M.Has_Key (Model (Container), Key))
 177
 178             --  It contains all the keys contained in Model
 179
 180             and (for all Key of Model (Container) =>
 181                   (for some L of Keys'Result => Equivalent_Keys (L, Key)))
 182
 183             --  It has no duplicate
 184
 185             and (for all I in 1 .. Length (Container) =>
 186                   (for all J in 1 .. Length (Container) =>
 187                     (if Equivalent_Keys
 188                           (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
 189                      then I = J)));
 190       pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
 191
 192       function Positions (Container : Map) return P.Map with
 193       --  The Positions map is used to model cursors. It only contains valid
 194       --  cursors and maps them to their position in the container.
 195
 196         Ghost,
 197         Global => null,
 198         Post   =>
 199           not P.Has_Key (Positions'Result, No_Element)
 200
 201             --  Positions of cursors are smaller than the container's length
 202
 203             and then
 204               (for all I of Positions'Result =>
 205                 P.Get (Positions'Result, I) in 1 .. Length (Container)
 206
 207             --  No two cursors have the same position. Note that we do not
 208             --  state that there is a cursor in the map for each position, as
 209             --  it is rarely needed.
 210
 211             and then
 212               (for all J of Positions'Result =>
 213                 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
 214                   then I = J)));
 215
 216       procedure Lift_Abstraction_Level (Container : Map) with
 217         --  Lift_Abstraction_Level is a ghost procedure that does nothing but
 218         --  assume that we can access the same elements by iterating over
 219         --  positions or cursors.
 220         --  This information is not generally useful except when switching from
 221         --  a low-level, cursor-aware view of a container, to a high-level,
 222         --  position-based view.
 223
 224         Ghost,
 225         Global => null,
 226         Post   =>
 227           (for all Key of Keys (Container) =>
 228             (for some I of Positions (Container) =>
 229               K.Get (Keys (Container), P.Get (Positions (Container), I)) =
 230                 Key));
 231
 232       function Contains
 233         (C : M.Map;
 234          K : Key_Type) return Boolean renames M.Has_Key;
 235       --  To improve readability of contracts, we rename the function used to
 236       --  search for a key in the model to Contains.
 237
 238       function Element
 239         (C : M.Map;
 240          K : Key_Type) return Element_Type renames M.Get;
 241       --  To improve readability of contracts, we rename the function used to
 242       --  access an element in the model to Element.
 243
 244    end Formal_Model;
 245    use Formal_Model;
 246
 247    function "=" (Left, Right : Map) return Boolean with
 248      Global => null,
 249      Post   => "="'Result = (Model (Left) = Model (Right));
 250
 251    function Capacity (Container : Map) return Count_Type with
 252      Global => null,
 253      Post   => Capacity'Result = Container.Capacity;
 254
 255    procedure Reserve_Capacity
 256      (Container : in out Map;
 257       Capacity  : Count_Type)
 258    with
 259      Global => null,
 260      Pre    => Capacity <= Container.Capacity,
 261      Post   => Model (Container) = Model (Container)'Old;
 262
 263    function Is_Empty (Container : Map) return Boolean with
 264      Global => null,
 265      Post   => Is_Empty'Result = M.Is_Empty (Model (Container));
 266
 267    procedure Clear (Container : in out Map) with
 268      Global => null,
 269      Post   => Length (Container) = 0 and M.Is_Empty (Model (Container));
 270
 271    procedure Assign (Target : in out Map; Source : Map) with
 272      Global => null,
 273      Pre    => Target.Capacity >= Length (Source),
 274      Post   =>
 275        Model (Target) = Model (Source)
 276          and Length (Source) = Length (Target)
 277
 278          --  Actual keys are preserved
 279
 280          and (for all Key of Keys (Source) =>
 281                Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
 282
 283    function Copy
 284      (Source   : Map;
 285       Capacity : Count_Type := 0) return Map
 286    with
 287      Global => null,
 288      Pre    => Capacity = 0 or else Capacity >= Source.Capacity,
 289      Post   =>
 290        Model (Copy'Result) = Model (Source)
 291          and Keys (Copy'Result) = Keys (Source)
 292          and Positions (Copy'Result) = Positions (Source)
 293          and (if Capacity = 0 then
 294                  Copy'Result.Capacity = Source.Capacity
 295               else
 296                  Copy'Result.Capacity = Capacity);
 297    --  Copy returns a container stricty equal to Source. It must have the same
 298    --  cursors associated with each element. Therefore:
 299    --  - capacity=0 means use Source.Capacity as capacity of target
 300    --  - the modulus cannot be changed.
 301
 302    function Key (Container : Map; Position : Cursor) return Key_Type with
 303      Global => null,
 304      Pre    => Has_Element (Container, Position),
 305      Post   =>
 306        Key'Result =
 307          K.Get (Keys (Container), P.Get (Positions (Container), Position));
 308    pragma Annotate (GNATprove, Inline_For_Proof, Key);
 309
 310    function Element
 311      (Container : Map;
 312       Position  : Cursor) return Element_Type
 313    with
 314      Global => null,
 315      Pre    => Has_Element (Container, Position),
 316      Post   =>
 317        Element'Result = Element (Model (Container), Key (Container, Position));
 318    pragma Annotate (GNATprove, Inline_For_Proof, Element);
 319
 320    procedure Replace_Element
 321      (Container : in out Map;
 322       Position  : Cursor;
 323       New_Item  : Element_Type)
 324    with
 325      Global => null,
 326      Pre    => Has_Element (Container, Position),
 327      Post   =>
 328
 329        --  Order of keys and cursors is preserved
 330
 331        Keys (Container) = Keys (Container)'Old
 332          and Positions (Container) = Positions (Container)'Old
 333
 334          --  New_Item is now associated with the key at position Position in
 335          --  Container.
 336
 337          and Element (Container, Position) = New_Item
 338
 339          --  Elements associated with other keys are preserved
 340
 341          and M.Same_Keys (Model (Container), Model (Container)'Old)
 342          and M.Elements_Equal_Except
 343                (Model (Container),
 344                 Model (Container)'Old,
 345                 Key (Container, Position));
 346
 347    procedure Move (Target : in out Map; Source : in out Map) with
 348      Global => null,
 349      Pre    => Target.Capacity >= Length (Source),
 350      Post   =>
 351        Model (Target) = Model (Source)'Old
 352          and Length (Source)'Old = Length (Target)
 353          and Length (Source) = 0
 354
 355          --  Actual keys are preserved
 356
 357          and (for all Key of Keys (Source)'Old =>
 358                Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
 359
 360    procedure Insert
 361      (Container : in out Map;
 362       Key       : Key_Type;
 363       New_Item  : Element_Type;
 364       Position  : out Cursor;
 365       Inserted  : out Boolean)
 366    with
 367      Global         => null,
 368      Pre            =>
 369        Length (Container) < Container.Capacity or Contains (Container, Key),
 370      Post           =>
 371        Contains (Container, Key)
 372          and Has_Element (Container, Position)
 373          and Equivalent_Keys
 374                (Formal_Hashed_Maps.Key (Container, Position), Key),
 375      Contract_Cases =>
 376
 377        --  If Key is already in Container, it is not modified and Inserted is
 378        --  set to False.
 379
 380        (Contains (Container, Key) =>
 381           not Inserted
 382             and Model (Container) = Model (Container)'Old
 383             and Keys (Container) = Keys (Container)'Old
 384             and Positions (Container) = Positions (Container)'Old,
 385
 386         --  Otherwise, Key is inserted in Container and Inserted is set to True
 387
 388         others =>
 389           Inserted
 390             and Length (Container) = Length (Container)'Old + 1
 391
 392             --  Key now maps to New_Item
 393
 394             and Formal_Hashed_Maps.Key (Container, Position) = Key
 395             and Element (Model (Container), Key) = New_Item
 396
 397             --  Other keys are preserved
 398
 399             and Model (Container)'Old <= Model (Container)
 400             and M.Keys_Included_Except
 401                   (Model (Container),
 402                    Model (Container)'Old,
 403                    Key)
 404
 405             --  Mapping from cursors to keys is preserved
 406
 407             and Mapping_Preserved
 408                   (K_Left  => Keys (Container)'Old,
 409                    K_Right => Keys (Container),
 410                    P_Left  => Positions (Container)'Old,
 411                    P_Right => Positions (Container))
 412             and P.Keys_Included_Except
 413                   (Positions (Container),
 414                    Positions (Container)'Old,
 415                    Position));
 416
 417    procedure Insert
 418      (Container : in out Map;
 419       Key       : Key_Type;
 420       New_Item  : Element_Type)
 421    with
 422      Global => null,
 423      Pre    =>
 424        Length (Container) < Container.Capacity
 425         and then (not Contains (Container, Key)),
 426      Post   =>
 427        Length (Container) = Length (Container)'Old + 1
 428          and Contains (Container, Key)
 429
 430          --  Key now maps to New_Item
 431
 432          and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
 433          and Element (Model (Container), Key) = New_Item
 434
 435          --  Other keys are preserved
 436
 437          and Model (Container)'Old <= Model (Container)
 438          and M.Keys_Included_Except
 439                (Model (Container),
 440                 Model (Container)'Old,
 441                 Key)
 442
 443          --  Mapping from cursors to keys is preserved
 444
 445          and Mapping_Preserved
 446                (K_Left  => Keys (Container)'Old,
 447                 K_Right => Keys (Container),
 448                 P_Left  => Positions (Container)'Old,
 449                 P_Right => Positions (Container))
 450          and P.Keys_Included_Except
 451                (Positions (Container),
 452                 Positions (Container)'Old,
 453                 Find (Container, Key));
 454
 455    procedure Include
 456      (Container : in out Map;
 457       Key       : Key_Type;
 458       New_Item  : Element_Type)
 459    with
 460      Global         => null,
 461      Pre            =>
 462        Length (Container) < Container.Capacity or Contains (Container, Key),
 463      Post           =>
 464        Contains (Container, Key) and Element (Container, Key) = New_Item,
 465      Contract_Cases =>
 466
 467        --  If Key is already in Container, Key is mapped to New_Item
 468
 469        (Contains (Container, Key) =>
 470
 471           --  Cursors are preserved
 472
 473           Positions (Container) = Positions (Container)'Old
 474
 475             --  The key equivalent to Key in Container is replaced by Key
 476
 477             and K.Get
 478                   (Keys (Container),
 479                    P.Get (Positions (Container), Find (Container, Key))) = Key
 480             and K.Equal_Except
 481                   (Keys (Container)'Old,
 482                    Keys (Container),
 483                    P.Get (Positions (Container), Find (Container, Key)))
 484
 485             --  Elements associated with other keys are preserved
 486
 487             and M.Same_Keys (Model (Container), Model (Container)'Old)
 488             and M.Elements_Equal_Except
 489                   (Model (Container),
 490                    Model (Container)'Old,
 491                    Key),
 492
 493         --  Otherwise, Key is inserted in Container
 494
 495         others =>
 496           Length (Container) = Length (Container)'Old + 1
 497
 498             --  Other keys are preserved
 499
 500             and Model (Container)'Old <= Model (Container)
 501             and M.Keys_Included_Except
 502                   (Model (Container),
 503                    Model (Container)'Old,
 504                    Key)
 505
 506             --  Mapping from cursors to keys is preserved
 507
 508             and Mapping_Preserved
 509                   (K_Left  => Keys (Container)'Old,
 510                    K_Right => Keys (Container),
 511                    P_Left  => Positions (Container)'Old,
 512                    P_Right => Positions (Container))
 513             and P.Keys_Included_Except
 514                   (Positions (Container),
 515                    Positions (Container)'Old,
 516                    Find (Container, Key)));
 517
 518    procedure Replace
 519      (Container : in out Map;
 520       Key       : Key_Type;
 521       New_Item  : Element_Type)
 522    with
 523      Global => null,
 524      Pre    => Contains (Container, Key),
 525      Post   =>
 526
 527        --  Cursors are preserved
 528
 529        Positions (Container) = Positions (Container)'Old
 530
 531          --  The key equivalent to Key in Container is replaced by Key
 532
 533          and K.Get
 534                (Keys (Container),
 535                 P.Get (Positions (Container), Find (Container, Key))) = Key
 536          and K.Equal_Except
 537                (Keys (Container)'Old,
 538                 Keys (Container),
 539                 P.Get (Positions (Container), Find (Container, Key)))
 540
 541          --  New_Item is now associated with the Key in Container
 542
 543          and Element (Model (Container), Key) = New_Item
 544
 545          --  Elements associated with other keys are preserved
 546
 547          and M.Same_Keys (Model (Container), Model (Container)'Old)
 548          and M.Elements_Equal_Except
 549                (Model (Container),
 550                 Model (Container)'Old,
 551                 Key);
 552
 553    procedure Exclude (Container : in out Map; Key : Key_Type) with
 554      Global         => null,
 555      Post           => not Contains (Container, Key),
 556      Contract_Cases =>
 557
 558        --  If Key is not in Container, nothing is changed
 559
 560        (not Contains (Container, Key) =>
 561           Model (Container) = Model (Container)'Old
 562             and Keys (Container) = Keys (Container)'Old
 563             and Positions (Container) = Positions (Container)'Old,
 564
 565         --  Otherwise, Key is removed from Container
 566
 567         others =>
 568           Length (Container) = Length (Container)'Old - 1
 569
 570             --  Other keys are preserved
 571
 572             and Model (Container) <= Model (Container)'Old
 573             and M.Keys_Included_Except
 574                   (Model (Container)'Old,
 575                    Model (Container),
 576                    Key)
 577
 578             --  Mapping from cursors to keys is preserved
 579
 580             and Mapping_Preserved
 581                   (K_Left  => Keys (Container),
 582                    K_Right => Keys (Container)'Old,
 583                    P_Left  => Positions (Container),
 584                    P_Right => Positions (Container)'Old)
 585             and P.Keys_Included_Except
 586                   (Positions (Container)'Old,
 587                    Positions (Container),
 588                    Find (Container, Key)'Old));
 589
 590    procedure Delete (Container : in out Map; Key : Key_Type) with
 591      Global => null,
 592      Pre    => Contains (Container, Key),
 593      Post   =>
 594        Length (Container) = Length (Container)'Old - 1
 595
 596          --  Key is no longer in Container
 597
 598          and not Contains (Container, Key)
 599
 600          --  Other keys are preserved
 601
 602          and Model (Container) <= Model (Container)'Old
 603          and M.Keys_Included_Except
 604                (Model (Container)'Old,
 605                 Model (Container),
 606                 Key)
 607
 608          --  Mapping from cursors to keys is preserved
 609
 610          and Mapping_Preserved
 611                (K_Left  => Keys (Container),
 612                 K_Right => Keys (Container)'Old,
 613                 P_Left  => Positions (Container),
 614                 P_Right => Positions (Container)'Old)
 615          and P.Keys_Included_Except
 616                (Positions (Container)'Old,
 617                 Positions (Container),
 618                 Find (Container, Key)'Old);
 619
 620    procedure Delete (Container : in out Map; Position : in out Cursor) with
 621      Global => null,
 622      Pre    => Has_Element (Container, Position),
 623      Post   =>
 624        Position = No_Element
 625          and Length (Container) = Length (Container)'Old - 1
 626
 627          --  The key at position Position is no longer in Container
 628
 629          and not Contains (Container, Key (Container, Position)'Old)
 630          and not P.Has_Key (Positions (Container), Position'Old)
 631
 632          --  Other keys are preserved
 633
 634          and Model (Container) <= Model (Container)'Old
 635          and M.Keys_Included_Except
 636                (Model (Container)'Old,
 637                 Model (Container),
 638                 Key (Container, Position)'Old)
 639
 640          --  Mapping from cursors to keys is preserved
 641
 642          and Mapping_Preserved
 643                (K_Left  => Keys (Container),
 644                 K_Right => Keys (Container)'Old,
 645                 P_Left  => Positions (Container),
 646                 P_Right => Positions (Container)'Old)
 647          and P.Keys_Included_Except
 648                (Positions (Container)'Old,
 649                 Positions (Container),
 650                 Position'Old);
 651
 652    function First (Container : Map) return Cursor with
 653      Global         => null,
 654      Contract_Cases =>
 655        (Length (Container) = 0 =>
 656           First'Result = No_Element,
 657
 658         others =>
 659           Has_Element (Container, First'Result)
 660             and P.Get (Positions (Container), First'Result) = 1);
 661
 662    function Next (Container : Map; Position : Cursor) return Cursor with
 663      Global         => null,
 664      Pre            =>
 665        Has_Element (Container, Position) or else Position = No_Element,
 666      Contract_Cases =>
 667        (Position = No_Element
 668           or else P.Get (Positions (Container), Position) = Length (Container)
 669         =>
 670           Next'Result = No_Element,
 671
 672         others =>
 673           Has_Element (Container, Next'Result)
 674             and then P.Get (Positions (Container), Next'Result) =
 675                      P.Get (Positions (Container), Position) + 1);
 676
 677    procedure Next (Container : Map; Position : in out Cursor) with
 678      Global         => null,
 679      Pre            =>
 680        Has_Element (Container, Position) or else Position = No_Element,
 681      Contract_Cases =>
 682        (Position = No_Element
 683           or else P.Get (Positions (Container), Position) = Length (Container)
 684         =>
 685           Position = No_Element,
 686
 687         others =>
 688           Has_Element (Container, Position)
 689             and then P.Get (Positions (Container), Position) =
 690                      P.Get (Positions (Container), Position'Old) + 1);
 691
 692    function Find (Container : Map; Key : Key_Type) return Cursor with
 693      Global         => null,
 694      Contract_Cases =>
 695
 696        --  If Key is not is not contained in Container, Find returns No_Element
 697
 698        (not Contains (Model (Container), Key) =>
 699           Find'Result = No_Element,
 700
 701         --  Otherwise, Find returns a valid cursor in Container
 702
 703         others =>
 704           P.Has_Key (Positions (Container), Find'Result)
 705
 706             --  The key designated by the result of Find is Key
 707
 708             and Equivalent_Keys
 709                   (Formal_Hashed_Maps.Key (Container, Find'Result), Key));
 710
 711    function Contains (Container : Map; Key : Key_Type) return Boolean with
 712      Global => null,
 713      Post   => Contains'Result = Contains (Model (Container), Key);
 714    pragma Annotate (GNATprove, Inline_For_Proof, Contains);
 715
 716    function Element (Container : Map; Key : Key_Type) return Element_Type with
 717      Global => null,
 718      Pre    => Contains (Container, Key),
 719      Post   => Element'Result = Element (Model (Container), Key);
 720    pragma Annotate (GNATprove, Inline_For_Proof, Element);
 721
 722    function Has_Element (Container : Map; Position : Cursor) return Boolean
 723    with
 724      Global => null,
 725      Post   =>
 726        Has_Element'Result = P.Has_Key (Positions (Container), Position);
 727    pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
 728
 729    function Default_Modulus (Capacity : Count_Type) return Hash_Type with
 730      Global => null;
 731
 732 private
 733    pragma SPARK_Mode (Off);
 734
 735    pragma Inline (Length);
 736    pragma Inline (Is_Empty);
 737    pragma Inline (Clear);
 738    pragma Inline (Key);
 739    pragma Inline (Element);
 740    pragma Inline (Contains);
 741    pragma Inline (Capacity);
 742    pragma Inline (Has_Element);
 743    pragma Inline (Equivalent_Keys);
 744    pragma Inline (Next);
 745
 746    type Node_Type is record
 747       Key         : Key_Type;
 748       Element     : Element_Type;
 749       Next        : Count_Type;
 750       Has_Element : Boolean := False;
 751    end record;
 752
 753    package HT_Types is new
 754      Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 755
 756    type Map (Capacity : Count_Type; Modulus : Hash_Type) is
 757      new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
 758
 759    use HT_Types;
 760
 761    Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
 762
 763 end Ada.Containers.Formal_Hashed_Maps;