gcc/ada/a-cofuma.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --                      ADA.CONTAINERS.FUNCTIONAL_MAPS                      --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2016-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 pragma Ada_2012;
  33 private with Ada.Containers.Functional_Base;
  34
  35 generic
  36    type Key_Type (<>) is private;
  37    type Element_Type (<>)  is private;
  38
  39    with function Equivalent_Keys
  40      (Left  : Key_Type;
  41       Right : Key_Type) return Boolean is "=";
  42
  43    Enable_Handling_Of_Equivalence : Boolean := True;
  44    --  This constant should only be set to False when no particular handling
  45    --  of equivalence over keys is needed, that is, Equivalent_Keys defines a
  46    --  key uniquely.
  47
  48 package Ada.Containers.Functional_Maps with SPARK_Mode is
  49
  50    type Map is private with
  51      Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
  52      Iterable                  => (First       => Iter_First,
  53                                    Next        => Iter_Next,
  54                                    Has_Element => Iter_Has_Element,
  55                                    Element     => Iter_Element);
  56    --  Maps are empty when default initialized.
  57    --  "For in" quantification over maps should not be used.
  58    --  "For of" quantification over maps iterates over keys.
  59    --  Note that, for proof, "for of" quantification is understood modulo
  60    --  equivalence (the range of quantification comprises all the keys that are
  61    --  equivalent to any key of the map).
  62
  63    -----------------------
  64    --  Basic operations --
  65    -----------------------
  66
  67    --  Maps are axiomatized using Has_Key and Get, encoding respectively the
  68    --  presence of a key in a map and an accessor to elements associated with
  69    --  its keys. The length of a map is also added to protect Add against
  70    --  overflows but it is not actually modeled.
  71
  72    function Has_Key (Container : Map; Key : Key_Type) return Boolean with
  73    --  Return True if Key is present in Container
  74
  75      Global => null,
  76      Post   =>
  77        (if Enable_Handling_Of_Equivalence then
  78
  79           --  Has_Key returns the same result on all equivalent keys
  80
  81           (if (for some K of Container => Equivalent_Keys (K, Key)) then
  82               Has_Key'Result));
  83
  84    function Get (Container : Map; Key : Key_Type) return Element_Type with
  85    --  Return the element associated with Key in Container
  86
  87      Global => null,
  88      Pre    => Has_Key (Container, Key),
  89      Post   =>
  90        (if Enable_Handling_Of_Equivalence then
  91
  92           --  Get returns the same result on all equivalent keys
  93
  94           Get'Result = W_Get (Container, Witness (Container, Key))
  95             and (for all K of Container =>
  96                   (Equivalent_Keys (K, Key) =
  97                     (Witness (Container, Key) = Witness (Container, K)))));
  98
  99    function Length (Container : Map) return Count_Type with
 100      Global => null;
 101    --  Return the number of mappings in Container
 102
 103    ------------------------
 104    -- Property Functions --
 105    ------------------------
 106
 107    function "<=" (Left : Map; Right : Map) return Boolean with
 108    --  Map inclusion
 109
 110      Global => null,
 111      Post   =>
 112        "<="'Result =
 113          (for all Key of Left =>
 114            Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
 115
 116    function "=" (Left : Map; Right : Map) return Boolean with
 117    --  Extensional equality over maps
 118
 119      Global => null,
 120      Post   =>
 121        "="'Result =
 122          ((for all Key of Left =>
 123             Has_Key (Right, Key)
 124               and then Get (Right, Key) = Get (Left, Key))
 125               and (for all Key of Right => Has_Key (Left, Key)));
 126
 127    pragma Warnings (Off, "unused variable ""Key""");
 128    function Is_Empty (Container : Map) return Boolean with
 129    --  A map is empty if it contains no key
 130
 131      Global => null,
 132      Post   => Is_Empty'Result = (for all Key of Container => False);
 133    pragma Warnings (On, "unused variable ""Key""");
 134
 135    function Keys_Included (Left : Map; Right : Map) return Boolean
 136    --  Returns True if every Key of Left is in Right
 137
 138    with
 139      Global => null,
 140      Post   =>
 141        Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
 142
 143    function Same_Keys (Left : Map; Right : Map) return Boolean
 144    --  Returns True if Left and Right have the same keys
 145
 146    with
 147      Global => null,
 148      Post   =>
 149        Same_Keys'Result =
 150          (Keys_Included (Left, Right)
 151            and Keys_Included (Left => Right, Right => Left));
 152    pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
 153
 154    function Keys_Included_Except
 155      (Left    : Map;
 156       Right   : Map;
 157       New_Key : Key_Type) return Boolean
 158    --  Returns True if Left contains only keys of Right and possibly New_Key
 159
 160    with
 161      Global => null,
 162      Post   =>
 163        Keys_Included_Except'Result =
 164          (for all Key of Left =>
 165            (if not Equivalent_Keys (Key, New_Key) then
 166                Has_Key (Right, Key)));
 167
 168    function Keys_Included_Except
 169      (Left  : Map;
 170       Right : Map;
 171       X     : Key_Type;
 172       Y     : Key_Type) return Boolean
 173    --  Returns True if Left contains only keys of Right and possibly X and Y
 174
 175    with
 176      Global => null,
 177      Post   =>
 178        Keys_Included_Except'Result =
 179          (for all Key of Left =>
 180            (if not Equivalent_Keys (Key, X)
 181               and not Equivalent_Keys (Key, Y)
 182             then
 183                Has_Key (Right, Key)));
 184
 185    function Elements_Equal_Except
 186      (Left    : Map;
 187       Right   : Map;
 188       New_Key : Key_Type) return Boolean
 189    --  Returns True if all the keys of Left are mapped to the same elements in
 190    --  Left and Right except New_Key.
 191
 192    with
 193      Global => null,
 194      Post   =>
 195        Elements_Equal_Except'Result =
 196          (for all Key of Left =>
 197            (if not Equivalent_Keys (Key, New_Key) then
 198                Has_Key (Right, Key)
 199                  and then Get (Left, Key) = Get (Right, Key)));
 200
 201    function Elements_Equal_Except
 202      (Left  : Map;
 203       Right : Map;
 204       X     : Key_Type;
 205       Y     : Key_Type) return Boolean
 206    --  Returns True if all the keys of Left are mapped to the same elements in
 207    --  Left and Right except X and Y.
 208
 209    with
 210      Global => null,
 211      Post   =>
 212        Elements_Equal_Except'Result =
 213          (for all Key of Left =>
 214            (if not Equivalent_Keys (Key, X)
 215               and not Equivalent_Keys (Key, Y)
 216             then
 217                Has_Key (Right, Key)
 218                  and then Get (Left, Key) = Get (Right, Key)));
 219
 220    ----------------------------
 221    -- Construction Functions --
 222    ----------------------------
 223
 224    --  For better efficiency of both proofs and execution, avoid using
 225    --  construction functions in annotations and rather use property functions.
 226
 227    function Add
 228      (Container : Map;
 229       New_Key   : Key_Type;
 230       New_Item  : Element_Type) return Map
 231    --  Returns Container augmented with the mapping Key -> New_Item
 232
 233    with
 234      Global => null,
 235      Pre    =>
 236        not Has_Key (Container, New_Key)
 237          and Length (Container) < Count_Type'Last,
 238      Post   =>
 239        Length (Container) + 1 = Length (Add'Result)
 240          and Has_Key (Add'Result, New_Key)
 241          and Get (Add'Result, New_Key) = New_Item
 242          and Container <= Add'Result
 243          and Keys_Included_Except (Add'Result, Container, New_Key);
 244
 245    function Set
 246      (Container : Map;
 247       Key       : Key_Type;
 248       New_Item  : Element_Type) return Map
 249    --  Returns Container, where the element associated with Key has been
 250    --  replaced by New_Item.
 251
 252    with
 253      Global => null,
 254      Pre    => Has_Key (Container, Key),
 255      Post   =>
 256        Length (Container) = Length (Set'Result)
 257          and Get (Set'Result, Key) = New_Item
 258          and Same_Keys (Container, Set'Result)
 259          and Elements_Equal_Except (Container, Set'Result, Key);
 260
 261    ------------------------------
 262    --  Handling of Equivalence --
 263    ------------------------------
 264
 265    --  These functions are used to specify that Get returns the same value on
 266    --  equivalent keys. They should not be used directly in user code.
 267
 268    function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
 269    with
 270      Ghost,
 271      Global => null;
 272    --  Returns True if there is a key with witness Witness in Container
 273
 274    function Witness (Container : Map; Key : Key_Type) return Count_Type with
 275    --  Returns the witness of Key in Container
 276
 277      Ghost,
 278      Global => null,
 279      Pre    => Has_Key (Container, Key),
 280      Post   => Has_Witness (Container, Witness'Result);
 281
 282    function W_Get (Container : Map; Witness : Count_Type) return Element_Type
 283    with
 284    --  Returns the element associated with a witness in Container
 285
 286      Ghost,
 287      Global => null,
 288      Pre    => Has_Witness (Container, Witness);
 289
 290    ---------------------------
 291    --  Iteration Primitives --
 292    ---------------------------
 293
 294    type Private_Key is private;
 295
 296    function Iter_First (Container : Map) return Private_Key with
 297      Global => null;
 298
 299    function Iter_Has_Element
 300      (Container : Map;
 301       Key       : Private_Key) return Boolean
 302    with
 303      Global => null;
 304
 305    function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
 306    with
 307      Global => null,
 308      Pre    => Iter_Has_Element (Container, Key);
 309
 310    function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
 311    with
 312      Global => null,
 313      Pre    => Iter_Has_Element (Container, Key);
 314    pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
 315
 316 private
 317
 318    pragma SPARK_Mode (Off);
 319
 320    function "="
 321      (Left  : Key_Type;
 322       Right : Key_Type) return Boolean renames Equivalent_Keys;
 323
 324    subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
 325
 326    package Element_Containers is new Ada.Containers.Functional_Base
 327      (Element_Type => Element_Type,
 328       Index_Type   => Positive_Count_Type);
 329
 330    package Key_Containers is new Ada.Containers.Functional_Base
 331      (Element_Type => Key_Type,
 332       Index_Type   => Positive_Count_Type);
 333
 334    type Map is record
 335       Keys     : Key_Containers.Container;
 336       Elements : Element_Containers.Container;
 337    end record;
 338
 339    type Private_Key is new Count_Type;
 340
 341    function Iter_First (Container : Map) return Private_Key is (1);
 342
 343    function Iter_Has_Element
 344      (Container : Map;
 345       Key       : Private_Key) return Boolean
 346    is
 347      (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
 348
 349    function Iter_Next
 350      (Container : Map;
 351       Key       : Private_Key) return Private_Key
 352    is
 353      (if Key = Private_Key'Last then 0 else Key + 1);
 354
 355    function Iter_Element
 356      (Container : Map;
 357       Key       : Private_Key) return Key_Type
 358    is
 359      (Key_Containers.Get (Container.Keys, Count_Type (Key)));
 360
 361 end Ada.Containers.Functional_Maps;