1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FUNCTIONAL_MAPS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2016-2018, 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 32pragma Ada_2012; 33private with Ada.Containers.Functional_Base; 34 35generic 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 48package 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 316private 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 361end Ada.Containers.Functional_Maps; 362