annotate gcc/ada/libgnat/a-cofuma.ads @ 131:84e7813d76e9

gcc-8.2
author mir3636
date Thu, 25 Oct 2018 07:37:49 +0900
parents 04ced10e8804
children 1830386684a0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
111
kono
parents:
diff changeset
1 ------------------------------------------------------------------------------
kono
parents:
diff changeset
2 -- --
kono
parents:
diff changeset
3 -- GNAT LIBRARY COMPONENTS --
kono
parents:
diff changeset
4 -- --
kono
parents:
diff changeset
5 -- ADA.CONTAINERS.FUNCTIONAL_MAPS --
kono
parents:
diff changeset
6 -- --
kono
parents:
diff changeset
7 -- S p e c --
kono
parents:
diff changeset
8 -- --
131
84e7813d76e9 gcc-8.2
mir3636
parents: 111
diff changeset
9 -- Copyright (C) 2016-2018, Free Software Foundation, Inc. --
111
kono
parents:
diff changeset
10 -- --
kono
parents:
diff changeset
11 -- This specification is derived from the Ada Reference Manual for use with --
kono
parents:
diff changeset
12 -- GNAT. The copyright notice above, and the license provisions that follow --
kono
parents:
diff changeset
13 -- apply solely to the contents of the part following the private keyword. --
kono
parents:
diff changeset
14 -- --
kono
parents:
diff changeset
15 -- GNAT is free software; you can redistribute it and/or modify it under --
kono
parents:
diff changeset
16 -- terms of the GNU General Public License as published by the Free Soft- --
kono
parents:
diff changeset
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
kono
parents:
diff changeset
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
kono
parents:
diff changeset
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
kono
parents:
diff changeset
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
kono
parents:
diff changeset
21 -- --
kono
parents:
diff changeset
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
kono
parents:
diff changeset
23 -- additional permissions described in the GCC Runtime Library Exception, --
kono
parents:
diff changeset
24 -- version 3.1, as published by the Free Software Foundation. --
kono
parents:
diff changeset
25 -- --
kono
parents:
diff changeset
26 -- You should have received a copy of the GNU General Public License and --
kono
parents:
diff changeset
27 -- a copy of the GCC Runtime Library Exception along with this program; --
kono
parents:
diff changeset
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
kono
parents:
diff changeset
29 -- <http://www.gnu.org/licenses/>. --
kono
parents:
diff changeset
30 ------------------------------------------------------------------------------
kono
parents:
diff changeset
31
kono
parents:
diff changeset
32 pragma Ada_2012;
kono
parents:
diff changeset
33 private with Ada.Containers.Functional_Base;
kono
parents:
diff changeset
34
kono
parents:
diff changeset
35 generic
kono
parents:
diff changeset
36 type Key_Type (<>) is private;
kono
parents:
diff changeset
37 type Element_Type (<>) is private;
kono
parents:
diff changeset
38
kono
parents:
diff changeset
39 with function Equivalent_Keys
kono
parents:
diff changeset
40 (Left : Key_Type;
kono
parents:
diff changeset
41 Right : Key_Type) return Boolean is "=";
kono
parents:
diff changeset
42
kono
parents:
diff changeset
43 Enable_Handling_Of_Equivalence : Boolean := True;
kono
parents:
diff changeset
44 -- This constant should only be set to False when no particular handling
kono
parents:
diff changeset
45 -- of equivalence over keys is needed, that is, Equivalent_Keys defines a
kono
parents:
diff changeset
46 -- key uniquely.
kono
parents:
diff changeset
47
kono
parents:
diff changeset
48 package Ada.Containers.Functional_Maps with SPARK_Mode is
kono
parents:
diff changeset
49
kono
parents:
diff changeset
50 type Map is private with
kono
parents:
diff changeset
51 Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
kono
parents:
diff changeset
52 Iterable => (First => Iter_First,
kono
parents:
diff changeset
53 Next => Iter_Next,
kono
parents:
diff changeset
54 Has_Element => Iter_Has_Element,
kono
parents:
diff changeset
55 Element => Iter_Element);
kono
parents:
diff changeset
56 -- Maps are empty when default initialized.
kono
parents:
diff changeset
57 -- "For in" quantification over maps should not be used.
kono
parents:
diff changeset
58 -- "For of" quantification over maps iterates over keys.
kono
parents:
diff changeset
59 -- Note that, for proof, "for of" quantification is understood modulo
kono
parents:
diff changeset
60 -- equivalence (the range of quantification comprises all the keys that are
kono
parents:
diff changeset
61 -- equivalent to any key of the map).
kono
parents:
diff changeset
62
kono
parents:
diff changeset
63 -----------------------
kono
parents:
diff changeset
64 -- Basic operations --
kono
parents:
diff changeset
65 -----------------------
kono
parents:
diff changeset
66
kono
parents:
diff changeset
67 -- Maps are axiomatized using Has_Key and Get, encoding respectively the
kono
parents:
diff changeset
68 -- presence of a key in a map and an accessor to elements associated with
kono
parents:
diff changeset
69 -- its keys. The length of a map is also added to protect Add against
kono
parents:
diff changeset
70 -- overflows but it is not actually modeled.
kono
parents:
diff changeset
71
kono
parents:
diff changeset
72 function Has_Key (Container : Map; Key : Key_Type) return Boolean with
kono
parents:
diff changeset
73 -- Return True if Key is present in Container
kono
parents:
diff changeset
74
kono
parents:
diff changeset
75 Global => null,
kono
parents:
diff changeset
76 Post =>
kono
parents:
diff changeset
77 (if Enable_Handling_Of_Equivalence then
kono
parents:
diff changeset
78
kono
parents:
diff changeset
79 -- Has_Key returns the same result on all equivalent keys
kono
parents:
diff changeset
80
kono
parents:
diff changeset
81 (if (for some K of Container => Equivalent_Keys (K, Key)) then
kono
parents:
diff changeset
82 Has_Key'Result));
kono
parents:
diff changeset
83
kono
parents:
diff changeset
84 function Get (Container : Map; Key : Key_Type) return Element_Type with
kono
parents:
diff changeset
85 -- Return the element associated with Key in Container
kono
parents:
diff changeset
86
kono
parents:
diff changeset
87 Global => null,
kono
parents:
diff changeset
88 Pre => Has_Key (Container, Key),
kono
parents:
diff changeset
89 Post =>
kono
parents:
diff changeset
90 (if Enable_Handling_Of_Equivalence then
kono
parents:
diff changeset
91
kono
parents:
diff changeset
92 -- Get returns the same result on all equivalent keys
kono
parents:
diff changeset
93
kono
parents:
diff changeset
94 Get'Result = W_Get (Container, Witness (Container, Key))
kono
parents:
diff changeset
95 and (for all K of Container =>
kono
parents:
diff changeset
96 (Equivalent_Keys (K, Key) =
kono
parents:
diff changeset
97 (Witness (Container, Key) = Witness (Container, K)))));
kono
parents:
diff changeset
98
kono
parents:
diff changeset
99 function Length (Container : Map) return Count_Type with
kono
parents:
diff changeset
100 Global => null;
kono
parents:
diff changeset
101 -- Return the number of mappings in Container
kono
parents:
diff changeset
102
kono
parents:
diff changeset
103 ------------------------
kono
parents:
diff changeset
104 -- Property Functions --
kono
parents:
diff changeset
105 ------------------------
kono
parents:
diff changeset
106
kono
parents:
diff changeset
107 function "<=" (Left : Map; Right : Map) return Boolean with
kono
parents:
diff changeset
108 -- Map inclusion
kono
parents:
diff changeset
109
kono
parents:
diff changeset
110 Global => null,
kono
parents:
diff changeset
111 Post =>
kono
parents:
diff changeset
112 "<="'Result =
kono
parents:
diff changeset
113 (for all Key of Left =>
kono
parents:
diff changeset
114 Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
kono
parents:
diff changeset
115
kono
parents:
diff changeset
116 function "=" (Left : Map; Right : Map) return Boolean with
kono
parents:
diff changeset
117 -- Extensional equality over maps
kono
parents:
diff changeset
118
kono
parents:
diff changeset
119 Global => null,
kono
parents:
diff changeset
120 Post =>
kono
parents:
diff changeset
121 "="'Result =
kono
parents:
diff changeset
122 ((for all Key of Left =>
kono
parents:
diff changeset
123 Has_Key (Right, Key)
kono
parents:
diff changeset
124 and then Get (Right, Key) = Get (Left, Key))
kono
parents:
diff changeset
125 and (for all Key of Right => Has_Key (Left, Key)));
kono
parents:
diff changeset
126
kono
parents:
diff changeset
127 pragma Warnings (Off, "unused variable ""Key""");
kono
parents:
diff changeset
128 function Is_Empty (Container : Map) return Boolean with
kono
parents:
diff changeset
129 -- A map is empty if it contains no key
kono
parents:
diff changeset
130
kono
parents:
diff changeset
131 Global => null,
kono
parents:
diff changeset
132 Post => Is_Empty'Result = (for all Key of Container => False);
kono
parents:
diff changeset
133 pragma Warnings (On, "unused variable ""Key""");
kono
parents:
diff changeset
134
kono
parents:
diff changeset
135 function Keys_Included (Left : Map; Right : Map) return Boolean
kono
parents:
diff changeset
136 -- Returns True if every Key of Left is in Right
kono
parents:
diff changeset
137
kono
parents:
diff changeset
138 with
kono
parents:
diff changeset
139 Global => null,
kono
parents:
diff changeset
140 Post =>
kono
parents:
diff changeset
141 Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
kono
parents:
diff changeset
142
kono
parents:
diff changeset
143 function Same_Keys (Left : Map; Right : Map) return Boolean
kono
parents:
diff changeset
144 -- Returns True if Left and Right have the same keys
kono
parents:
diff changeset
145
kono
parents:
diff changeset
146 with
kono
parents:
diff changeset
147 Global => null,
kono
parents:
diff changeset
148 Post =>
kono
parents:
diff changeset
149 Same_Keys'Result =
kono
parents:
diff changeset
150 (Keys_Included (Left, Right)
kono
parents:
diff changeset
151 and Keys_Included (Left => Right, Right => Left));
kono
parents:
diff changeset
152 pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
kono
parents:
diff changeset
153
kono
parents:
diff changeset
154 function Keys_Included_Except
kono
parents:
diff changeset
155 (Left : Map;
kono
parents:
diff changeset
156 Right : Map;
kono
parents:
diff changeset
157 New_Key : Key_Type) return Boolean
kono
parents:
diff changeset
158 -- Returns True if Left contains only keys of Right and possibly New_Key
kono
parents:
diff changeset
159
kono
parents:
diff changeset
160 with
kono
parents:
diff changeset
161 Global => null,
kono
parents:
diff changeset
162 Post =>
kono
parents:
diff changeset
163 Keys_Included_Except'Result =
kono
parents:
diff changeset
164 (for all Key of Left =>
kono
parents:
diff changeset
165 (if not Equivalent_Keys (Key, New_Key) then
kono
parents:
diff changeset
166 Has_Key (Right, Key)));
kono
parents:
diff changeset
167
kono
parents:
diff changeset
168 function Keys_Included_Except
kono
parents:
diff changeset
169 (Left : Map;
kono
parents:
diff changeset
170 Right : Map;
kono
parents:
diff changeset
171 X : Key_Type;
kono
parents:
diff changeset
172 Y : Key_Type) return Boolean
kono
parents:
diff changeset
173 -- Returns True if Left contains only keys of Right and possibly X and Y
kono
parents:
diff changeset
174
kono
parents:
diff changeset
175 with
kono
parents:
diff changeset
176 Global => null,
kono
parents:
diff changeset
177 Post =>
kono
parents:
diff changeset
178 Keys_Included_Except'Result =
kono
parents:
diff changeset
179 (for all Key of Left =>
kono
parents:
diff changeset
180 (if not Equivalent_Keys (Key, X)
kono
parents:
diff changeset
181 and not Equivalent_Keys (Key, Y)
kono
parents:
diff changeset
182 then
kono
parents:
diff changeset
183 Has_Key (Right, Key)));
kono
parents:
diff changeset
184
kono
parents:
diff changeset
185 function Elements_Equal_Except
kono
parents:
diff changeset
186 (Left : Map;
kono
parents:
diff changeset
187 Right : Map;
kono
parents:
diff changeset
188 New_Key : Key_Type) return Boolean
kono
parents:
diff changeset
189 -- Returns True if all the keys of Left are mapped to the same elements in
kono
parents:
diff changeset
190 -- Left and Right except New_Key.
kono
parents:
diff changeset
191
kono
parents:
diff changeset
192 with
kono
parents:
diff changeset
193 Global => null,
kono
parents:
diff changeset
194 Post =>
kono
parents:
diff changeset
195 Elements_Equal_Except'Result =
kono
parents:
diff changeset
196 (for all Key of Left =>
kono
parents:
diff changeset
197 (if not Equivalent_Keys (Key, New_Key) then
kono
parents:
diff changeset
198 Has_Key (Right, Key)
kono
parents:
diff changeset
199 and then Get (Left, Key) = Get (Right, Key)));
kono
parents:
diff changeset
200
kono
parents:
diff changeset
201 function Elements_Equal_Except
kono
parents:
diff changeset
202 (Left : Map;
kono
parents:
diff changeset
203 Right : Map;
kono
parents:
diff changeset
204 X : Key_Type;
kono
parents:
diff changeset
205 Y : Key_Type) return Boolean
kono
parents:
diff changeset
206 -- Returns True if all the keys of Left are mapped to the same elements in
kono
parents:
diff changeset
207 -- Left and Right except X and Y.
kono
parents:
diff changeset
208
kono
parents:
diff changeset
209 with
kono
parents:
diff changeset
210 Global => null,
kono
parents:
diff changeset
211 Post =>
kono
parents:
diff changeset
212 Elements_Equal_Except'Result =
kono
parents:
diff changeset
213 (for all Key of Left =>
kono
parents:
diff changeset
214 (if not Equivalent_Keys (Key, X)
kono
parents:
diff changeset
215 and not Equivalent_Keys (Key, Y)
kono
parents:
diff changeset
216 then
kono
parents:
diff changeset
217 Has_Key (Right, Key)
kono
parents:
diff changeset
218 and then Get (Left, Key) = Get (Right, Key)));
kono
parents:
diff changeset
219
kono
parents:
diff changeset
220 ----------------------------
kono
parents:
diff changeset
221 -- Construction Functions --
kono
parents:
diff changeset
222 ----------------------------
kono
parents:
diff changeset
223
kono
parents:
diff changeset
224 -- For better efficiency of both proofs and execution, avoid using
kono
parents:
diff changeset
225 -- construction functions in annotations and rather use property functions.
kono
parents:
diff changeset
226
kono
parents:
diff changeset
227 function Add
kono
parents:
diff changeset
228 (Container : Map;
kono
parents:
diff changeset
229 New_Key : Key_Type;
kono
parents:
diff changeset
230 New_Item : Element_Type) return Map
kono
parents:
diff changeset
231 -- Returns Container augmented with the mapping Key -> New_Item
kono
parents:
diff changeset
232
kono
parents:
diff changeset
233 with
kono
parents:
diff changeset
234 Global => null,
kono
parents:
diff changeset
235 Pre =>
kono
parents:
diff changeset
236 not Has_Key (Container, New_Key)
kono
parents:
diff changeset
237 and Length (Container) < Count_Type'Last,
kono
parents:
diff changeset
238 Post =>
kono
parents:
diff changeset
239 Length (Container) + 1 = Length (Add'Result)
kono
parents:
diff changeset
240 and Has_Key (Add'Result, New_Key)
kono
parents:
diff changeset
241 and Get (Add'Result, New_Key) = New_Item
kono
parents:
diff changeset
242 and Container <= Add'Result
kono
parents:
diff changeset
243 and Keys_Included_Except (Add'Result, Container, New_Key);
kono
parents:
diff changeset
244
kono
parents:
diff changeset
245 function Set
kono
parents:
diff changeset
246 (Container : Map;
kono
parents:
diff changeset
247 Key : Key_Type;
kono
parents:
diff changeset
248 New_Item : Element_Type) return Map
kono
parents:
diff changeset
249 -- Returns Container, where the element associated with Key has been
kono
parents:
diff changeset
250 -- replaced by New_Item.
kono
parents:
diff changeset
251
kono
parents:
diff changeset
252 with
kono
parents:
diff changeset
253 Global => null,
kono
parents:
diff changeset
254 Pre => Has_Key (Container, Key),
kono
parents:
diff changeset
255 Post =>
kono
parents:
diff changeset
256 Length (Container) = Length (Set'Result)
kono
parents:
diff changeset
257 and Get (Set'Result, Key) = New_Item
kono
parents:
diff changeset
258 and Same_Keys (Container, Set'Result)
kono
parents:
diff changeset
259 and Elements_Equal_Except (Container, Set'Result, Key);
kono
parents:
diff changeset
260
kono
parents:
diff changeset
261 ------------------------------
kono
parents:
diff changeset
262 -- Handling of Equivalence --
kono
parents:
diff changeset
263 ------------------------------
kono
parents:
diff changeset
264
kono
parents:
diff changeset
265 -- These functions are used to specify that Get returns the same value on
kono
parents:
diff changeset
266 -- equivalent keys. They should not be used directly in user code.
kono
parents:
diff changeset
267
kono
parents:
diff changeset
268 function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
kono
parents:
diff changeset
269 with
kono
parents:
diff changeset
270 Ghost,
kono
parents:
diff changeset
271 Global => null;
kono
parents:
diff changeset
272 -- Returns True if there is a key with witness Witness in Container
kono
parents:
diff changeset
273
kono
parents:
diff changeset
274 function Witness (Container : Map; Key : Key_Type) return Count_Type with
kono
parents:
diff changeset
275 -- Returns the witness of Key in Container
kono
parents:
diff changeset
276
kono
parents:
diff changeset
277 Ghost,
kono
parents:
diff changeset
278 Global => null,
kono
parents:
diff changeset
279 Pre => Has_Key (Container, Key),
kono
parents:
diff changeset
280 Post => Has_Witness (Container, Witness'Result);
kono
parents:
diff changeset
281
kono
parents:
diff changeset
282 function W_Get (Container : Map; Witness : Count_Type) return Element_Type
kono
parents:
diff changeset
283 with
kono
parents:
diff changeset
284 -- Returns the element associated with a witness in Container
kono
parents:
diff changeset
285
kono
parents:
diff changeset
286 Ghost,
kono
parents:
diff changeset
287 Global => null,
kono
parents:
diff changeset
288 Pre => Has_Witness (Container, Witness);
kono
parents:
diff changeset
289
kono
parents:
diff changeset
290 ---------------------------
kono
parents:
diff changeset
291 -- Iteration Primitives --
kono
parents:
diff changeset
292 ---------------------------
kono
parents:
diff changeset
293
kono
parents:
diff changeset
294 type Private_Key is private;
kono
parents:
diff changeset
295
kono
parents:
diff changeset
296 function Iter_First (Container : Map) return Private_Key with
kono
parents:
diff changeset
297 Global => null;
kono
parents:
diff changeset
298
kono
parents:
diff changeset
299 function Iter_Has_Element
kono
parents:
diff changeset
300 (Container : Map;
kono
parents:
diff changeset
301 Key : Private_Key) return Boolean
kono
parents:
diff changeset
302 with
kono
parents:
diff changeset
303 Global => null;
kono
parents:
diff changeset
304
kono
parents:
diff changeset
305 function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
kono
parents:
diff changeset
306 with
kono
parents:
diff changeset
307 Global => null,
kono
parents:
diff changeset
308 Pre => Iter_Has_Element (Container, Key);
kono
parents:
diff changeset
309
kono
parents:
diff changeset
310 function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
kono
parents:
diff changeset
311 with
kono
parents:
diff changeset
312 Global => null,
kono
parents:
diff changeset
313 Pre => Iter_Has_Element (Container, Key);
kono
parents:
diff changeset
314 pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
kono
parents:
diff changeset
315
kono
parents:
diff changeset
316 private
kono
parents:
diff changeset
317
kono
parents:
diff changeset
318 pragma SPARK_Mode (Off);
kono
parents:
diff changeset
319
kono
parents:
diff changeset
320 function "="
kono
parents:
diff changeset
321 (Left : Key_Type;
kono
parents:
diff changeset
322 Right : Key_Type) return Boolean renames Equivalent_Keys;
kono
parents:
diff changeset
323
kono
parents:
diff changeset
324 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
kono
parents:
diff changeset
325
kono
parents:
diff changeset
326 package Element_Containers is new Ada.Containers.Functional_Base
kono
parents:
diff changeset
327 (Element_Type => Element_Type,
kono
parents:
diff changeset
328 Index_Type => Positive_Count_Type);
kono
parents:
diff changeset
329
kono
parents:
diff changeset
330 package Key_Containers is new Ada.Containers.Functional_Base
kono
parents:
diff changeset
331 (Element_Type => Key_Type,
kono
parents:
diff changeset
332 Index_Type => Positive_Count_Type);
kono
parents:
diff changeset
333
kono
parents:
diff changeset
334 type Map is record
kono
parents:
diff changeset
335 Keys : Key_Containers.Container;
kono
parents:
diff changeset
336 Elements : Element_Containers.Container;
kono
parents:
diff changeset
337 end record;
kono
parents:
diff changeset
338
kono
parents:
diff changeset
339 type Private_Key is new Count_Type;
kono
parents:
diff changeset
340
kono
parents:
diff changeset
341 function Iter_First (Container : Map) return Private_Key is (1);
kono
parents:
diff changeset
342
kono
parents:
diff changeset
343 function Iter_Has_Element
kono
parents:
diff changeset
344 (Container : Map;
kono
parents:
diff changeset
345 Key : Private_Key) return Boolean
kono
parents:
diff changeset
346 is
kono
parents:
diff changeset
347 (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
kono
parents:
diff changeset
348
kono
parents:
diff changeset
349 function Iter_Next
kono
parents:
diff changeset
350 (Container : Map;
kono
parents:
diff changeset
351 Key : Private_Key) return Private_Key
kono
parents:
diff changeset
352 is
kono
parents:
diff changeset
353 (if Key = Private_Key'Last then 0 else Key + 1);
kono
parents:
diff changeset
354
kono
parents:
diff changeset
355 function Iter_Element
kono
parents:
diff changeset
356 (Container : Map;
kono
parents:
diff changeset
357 Key : Private_Key) return Key_Type
kono
parents:
diff changeset
358 is
kono
parents:
diff changeset
359 (Key_Containers.Get (Container.Keys, Count_Type (Key)));
kono
parents:
diff changeset
360
kono
parents:
diff changeset
361 end Ada.Containers.Functional_Maps;