Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cofuma.ads @ 111:04ced10e8804

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
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;