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    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
  39 package Ada.Containers.Functional_Maps with SPARK_Mode is
  40
  41    type Map is private with
  42      Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
  43      Iterable                  => (First       => Iter_First,
  44                                    Next        => Iter_Next,
  45                                    Has_Element => Iter_Has_Element,
  46                                    Element     => Iter_Element);
  47    --  Maps are empty when default initialized.
  48    --  "For in" quantification over maps should not be used.
  49    --  "For of" quantification over maps iterates over keys.
  50
  51    -----------------------
  52    --  Basic operations --
  53    -----------------------
  54
  55    --  Maps are axiomatized using Has_Key and Get, encoding respectively the
  56    --  presence of a key in a map and an accessor to elements associated to its
  57    --  keys. The length of a map is also added to protect Add against overflows
  58    --  but it is not actually modeled.
  59
  60    function Has_Key (Container : Map; Key : Key_Type) return Boolean with
  61      Global => null;
  62    --  Return True if Key is present in Container
  63
  64    function Get (Container : Map; Key : Key_Type) return Element_Type with
  65      Global => null,
  66      Pre    => Has_Key (Container, Key);
  67    --  Return the element associated to Key is present in Container
  68
  69    function Length (Container : Map) return Count_Type with
  70      Global => null;
  71    --  Return the number of mappings in Container
  72
  73    ------------------------
  74    -- Property Functions --
  75    ------------------------
  76
  77    function "<=" (Left : Map; Right : Map) return Boolean with
  78    --  Map inclusion
  79
  80      Global => null,
  81      Post   =>
  82        "<="'Result =
  83          (for all Key of Left =>
  84             Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
  85
  86    function "=" (Left : Map; Right : Map) return Boolean with
  87    --  Extensional equality over maps
  88
  89      Global => null,
  90      Post   =>
  91        "="'Result =
  92          ((for all Key of Left =>
  93                    Has_Key (Right, Key)
  94            and then Get (Right, Key) = Get (Left, Key))
  95           and (for all Key of Right => Has_Key (Left, Key)));
  96
  97    pragma Warnings (Off, "unused variable ""Key""");
  98    function Is_Empty (Container : Map) return Boolean with
  99    --  A map is empty if it contains no key
 100
 101      Global => null,
 102      Post   => Is_Empty'Result = (for all Key of Container => False);
 103    pragma Warnings (On, "unused variable ""Key""");
 104
 105    function Keys_Included (Left : Map; Right : Map) return Boolean
 106    --  Returns True if every Key of Left is in Right
 107
 108    with
 109      Global => null,
 110      Post   =>
 111        Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
 112
 113    function Same_Keys (Left : Map; Right : Map) return Boolean
 114    --  Returns True if Left and Right have the same keys
 115
 116    with
 117      Global => null,
 118      Post   =>
 119        Same_Keys'Result =
 120            (Keys_Included (Left, Right)
 121             and Keys_Included (Left => Right, Right => Left));
 122    pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
 123
 124    function Keys_Included_Except
 125      (Left    : Map;
 126       Right   : Map;
 127       New_Key : Key_Type) return Boolean
 128    --  Returns True if Left contains only keys of Right and possibly New_Key
 129
 130    with
 131      Global => null,
 132      Post   =>
 133          Keys_Included_Except'Result =
 134            (for all Key of Left =>
 135               (if not Equivalent_Keys (Key, New_Key)
 136                then Has_Key (Right, Key)));
 137
 138    function Keys_Included_Except
 139      (Left  : Map;
 140       Right : Map;
 141       X, Y  : Key_Type) return Boolean
 142    --  Returns True if Left contains only keys of Right and possibly X and Y
 143
 144    with
 145      Global => null,
 146      Post   =>
 147          Keys_Included_Except'Result =
 148            (for all Key of Left =>
 149               (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y)
 150                then Has_Key (Right, Key)));
 151
 152    function Elements_Equal_Except
 153      (Left    : Map;
 154       Right   : Map;
 155       New_Key : Key_Type) return Boolean
 156    --  Returns True if all the keys of Left are mapped to the same elements in
 157    --  Left and Right except New_Key.
 158
 159    with
 160      Global => null,
 161      Pre    => Keys_Included_Except (Left, Right, New_Key),
 162      Post   =>
 163        Elements_Equal_Except'Result =
 164          (for all Key of Left =>
 165             (if not Equivalent_Keys (Key, New_Key)
 166              then Get (Left, Key) = Get (Right, Key)));
 167
 168    function Elements_Equal_Except
 169      (Left  : Map;
 170       Right : Map;
 171       X, Y  : Key_Type) return Boolean
 172    --  Returns True if all the keys of Left are mapped to the same elements in
 173    --  Left and Right except X and Y.
 174
 175    with
 176      Global => null,
 177      Pre    => Keys_Included_Except (Left, Right, X, Y),
 178      Post   =>
 179        Elements_Equal_Except'Result =
 180          (for all Key of Left =>
 181             (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y)
 182              then Get (Left, Key) = Get (Right, Key)));
 183
 184    ----------------------------
 185    -- Construction Functions --
 186    ----------------------------
 187
 188    --  For better efficiency of both proofs and execution, avoid using
 189    --  construction functions in annotations and rather use property functions.
 190
 191    function Add
 192      (Container : Map;
 193       New_Key   : Key_Type;
 194       New_Item  : Element_Type) return Map
 195    --  Returns Container augmented with the mapping Key -> New_Item.
 196
 197    with
 198      Global => null,
 199      Pre    =>
 200          not Has_Key (Container, New_Key)
 201        and Length (Container) < Count_Type'Last,
 202      Post   =>
 203        Length (Container) + 1 = Length (Add'Result)
 204        and Has_Key (Add'Result, New_Key)
 205        and Get (Add'Result, New_Key) = New_Item
 206        and Container <= Add'Result
 207        and Keys_Included_Except (Add'Result, Container, New_Key);
 208
 209    function Set
 210      (Container : Map;
 211       Key       : Key_Type;
 212       New_Item  : Element_Type) return Map
 213    --  Returns Container, where the element associated to Key has been replaced
 214    --  by New_Item.
 215
 216    with
 217      Global => null,
 218      Pre    => Has_Key (Container, Key),
 219      Post   =>
 220        Length (Container) = Length (Set'Result)
 221        and Get (Set'Result, Key) = New_Item
 222        and Same_Keys (Container, Set'Result)
 223        and Elements_Equal_Except (Container, Set'Result, Key);
 224
 225    ---------------------------
 226    --  Iteration Primitives --
 227    ---------------------------
 228
 229    type Private_Key is private;
 230
 231    function Iter_First (Container : Map) return Private_Key with
 232      Global => null;
 233
 234    function Iter_Has_Element
 235      (Container : Map;
 236       Key       : Private_Key) return Boolean
 237    with
 238      Global => null;
 239
 240    function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
 241    with
 242      Global => null,
 243      Pre    => Iter_Has_Element (Container, Key);
 244
 245    function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
 246    with
 247      Global => null,
 248      Pre    => Iter_Has_Element (Container, Key);
 249    pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
 250
 251 private
 252
 253    pragma SPARK_Mode (Off);
 254
 255    function "="
 256      (Left  : Key_Type;
 257       Right : Key_Type) return Boolean renames Equivalent_Keys;
 258
 259    subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
 260
 261    package Element_Containers is new Ada.Containers.Functional_Base
 262      (Element_Type => Element_Type,
 263       Index_Type   => Positive_Count_Type);
 264
 265    package Key_Containers is new Ada.Containers.Functional_Base
 266      (Element_Type => Key_Type,
 267       Index_Type   => Positive_Count_Type);
 268
 269    type Map is record
 270       Keys     : Key_Containers.Container;
 271       Elements : Element_Containers.Container;
 272    end record;
 273
 274    type Private_Key is new Count_Type;
 275
 276    function Iter_First (Container : Map) return Private_Key is (1);
 277
 278    function Iter_Has_Element
 279      (Container : Map;
 280       Key       : Private_Key) return Boolean
 281    is
 282      (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
 283
 284    function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
 285    is
 286      (if Key = Private_Key'Last then 0 else Key + 1);
 287
 288    function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
 289    is
 290      (Key_Containers.Get (Container.Keys, Count_Type (Key)));
 291
 292 end Ada.Containers.Functional_Maps;