comparison gcc/ada/libgnat/a-cofuma.ads @ 145:1830386684a0

gcc-9.2.0
author anatofuz
date Thu, 13 Feb 2020 11:34:05 +0900
parents 84e7813d76e9
children
comparison
equal deleted inserted replaced
131:84e7813d76e9 145:1830386684a0
4 -- -- 4 -- --
5 -- ADA.CONTAINERS.FUNCTIONAL_MAPS -- 5 -- ADA.CONTAINERS.FUNCTIONAL_MAPS --
6 -- -- 6 -- --
7 -- S p e c -- 7 -- S p e c --
8 -- -- 8 -- --
9 -- Copyright (C) 2016-2018, Free Software Foundation, Inc. -- 9 -- Copyright (C) 2016-2019, Free Software Foundation, Inc. --
10 -- -- 10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with -- 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 -- 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. -- 13 -- apply solely to the contents of the part following the private keyword. --
14 -- -- 14 -- --
37 type Element_Type (<>) is private; 37 type Element_Type (<>) is private;
38 38
39 with function Equivalent_Keys 39 with function Equivalent_Keys
40 (Left : Key_Type; 40 (Left : Key_Type;
41 Right : Key_Type) return Boolean is "="; 41 Right : Key_Type) return Boolean is "=";
42 with function "=" (Left, Right : Element_Type) return Boolean is <>;
42 43
43 Enable_Handling_Of_Equivalence : Boolean := True; 44 Enable_Handling_Of_Equivalence : Boolean := True;
44 -- This constant should only be set to False when no particular handling 45 -- 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 -- of equivalence over keys is needed, that is, Equivalent_Keys defines a
46 -- key uniquely. 47 -- key uniquely.
240 and Has_Key (Add'Result, New_Key) 241 and Has_Key (Add'Result, New_Key)
241 and Get (Add'Result, New_Key) = New_Item 242 and Get (Add'Result, New_Key) = New_Item
242 and Container <= Add'Result 243 and Container <= Add'Result
243 and Keys_Included_Except (Add'Result, Container, New_Key); 244 and Keys_Included_Except (Add'Result, Container, New_Key);
244 245
246 function Remove
247 (Container : Map;
248 Key : Key_Type) return Map
249 -- Returns Container without any mapping for Key
250
251 with
252 Global => null,
253 Pre => Has_Key (Container, Key),
254 Post =>
255 Length (Container) = Length (Remove'Result) + 1
256 and not Has_Key (Remove'Result, Key)
257 and Remove'Result <= Container
258 and Keys_Included_Except (Container, Remove'Result, Key);
259
245 function Set 260 function Set
246 (Container : Map; 261 (Container : Map;
247 Key : Key_Type; 262 Key : Key_Type;
248 New_Item : Element_Type) return Map 263 New_Item : Element_Type) return Map
249 -- Returns Container, where the element associated with Key has been 264 -- Returns Container, where the element associated with Key has been