|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- ADA.CONTAINERS.FUNCTIONAL_SETS --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2016-2019, Free Software Foundation, Inc. --
|
|
111
|
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 Element_Type (<>) is private;
|
|
|
37
|
|
|
38 with function Equivalent_Elements
|
|
|
39 (Left : Element_Type;
|
|
|
40 Right : Element_Type) return Boolean is "=";
|
|
|
41
|
|
|
42 Enable_Handling_Of_Equivalence : Boolean := True;
|
|
|
43 -- This constant should only be set to False when no particular handling
|
|
|
44 -- of equivalence over elements is needed, that is, Equivalent_Elements
|
|
|
45 -- defines an element uniquely.
|
|
|
46
|
|
|
47 package Ada.Containers.Functional_Sets with SPARK_Mode is
|
|
|
48
|
|
|
49 type Set is private with
|
|
|
50 Default_Initial_Condition => Is_Empty (Set),
|
|
|
51 Iterable => (First => Iter_First,
|
|
|
52 Next => Iter_Next,
|
|
|
53 Has_Element => Iter_Has_Element,
|
|
|
54 Element => Iter_Element);
|
|
|
55 -- Sets are empty when default initialized.
|
|
|
56 -- "For in" quantification over sets should not be used.
|
|
|
57 -- "For of" quantification over sets iterates over elements.
|
|
|
58 -- Note that, for proof, "for of" quantification is understood modulo
|
|
|
59 -- equivalence (the range of quantification comprises all the elements that
|
|
|
60 -- are equivalent to any element of the set).
|
|
|
61
|
|
|
62 -----------------------
|
|
|
63 -- Basic operations --
|
|
|
64 -----------------------
|
|
|
65
|
|
|
66 -- Sets are axiomatized using Contains, which encodes whether an element is
|
|
|
67 -- contained in a set. The length of a set is also added to protect Add
|
|
|
68 -- against overflows but it is not actually modeled.
|
|
|
69
|
|
|
70 function Contains (Container : Set; Item : Element_Type) return Boolean with
|
|
|
71 -- Return True if Item is contained in Container
|
|
|
72
|
|
|
73 Global => null,
|
|
|
74 Post =>
|
|
|
75 (if Enable_Handling_Of_Equivalence then
|
|
|
76
|
|
|
77 -- Contains returns the same result on all equivalent elements
|
|
|
78
|
|
|
79 (if (for some E of Container => Equivalent_Elements (E, Item)) then
|
|
|
80 Contains'Result));
|
|
|
81
|
|
|
82 function Length (Container : Set) return Count_Type with
|
|
|
83 Global => null;
|
|
|
84 -- Return the number of elements in Container
|
|
|
85
|
|
|
86 ------------------------
|
|
|
87 -- Property Functions --
|
|
|
88 ------------------------
|
|
|
89
|
|
|
90 function "<=" (Left : Set; Right : Set) return Boolean with
|
|
|
91 -- Set inclusion
|
|
|
92
|
|
|
93 Global => null,
|
|
|
94 Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
|
|
|
95
|
|
|
96 function "=" (Left : Set; Right : Set) return Boolean with
|
|
|
97 -- Extensional equality over sets
|
|
|
98
|
|
|
99 Global => null,
|
|
|
100 Post => "="'Result = (Left <= Right and Right <= Left);
|
|
|
101
|
|
|
102 pragma Warnings (Off, "unused variable ""Item""");
|
|
|
103 function Is_Empty (Container : Set) return Boolean with
|
|
|
104 -- A set is empty if it contains no element
|
|
|
105
|
|
|
106 Global => null,
|
|
|
107 Post =>
|
|
|
108 Is_Empty'Result = (for all Item of Container => False)
|
|
|
109 and Is_Empty'Result = (Length (Container) = 0);
|
|
|
110 pragma Warnings (On, "unused variable ""Item""");
|
|
|
111
|
|
|
112 function Included_Except
|
|
|
113 (Left : Set;
|
|
|
114 Right : Set;
|
|
|
115 Item : Element_Type) return Boolean
|
|
|
116 -- Return True if Left contains only elements of Right except possibly
|
|
|
117 -- Item.
|
|
|
118
|
|
|
119 with
|
|
|
120 Global => null,
|
|
|
121 Post =>
|
|
|
122 Included_Except'Result =
|
|
|
123 (for all E of Left =>
|
|
|
124 Contains (Right, E) or Equivalent_Elements (E, Item));
|
|
|
125
|
|
|
126 function Includes_Intersection
|
|
|
127 (Container : Set;
|
|
|
128 Left : Set;
|
|
|
129 Right : Set) return Boolean
|
|
|
130 with
|
|
|
131 -- Return True if every element of the intersection of Left and Right is
|
|
|
132 -- in Container.
|
|
|
133
|
|
|
134 Global => null,
|
|
|
135 Post =>
|
|
|
136 Includes_Intersection'Result =
|
|
|
137 (for all Item of Left =>
|
|
|
138 (if Contains (Right, Item) then Contains (Container, Item)));
|
|
|
139
|
|
|
140 function Included_In_Union
|
|
|
141 (Container : Set;
|
|
|
142 Left : Set;
|
|
|
143 Right : Set) return Boolean
|
|
|
144 with
|
|
|
145 -- Return True if every element of Container is the union of Left and Right
|
|
|
146
|
|
|
147 Global => null,
|
|
|
148 Post =>
|
|
|
149 Included_In_Union'Result =
|
|
|
150 (for all Item of Container =>
|
|
|
151 Contains (Left, Item) or Contains (Right, Item));
|
|
|
152
|
|
|
153 function Is_Singleton
|
|
|
154 (Container : Set;
|
|
|
155 New_Item : Element_Type) return Boolean
|
|
|
156 with
|
|
|
157 -- Return True Container only contains New_Item
|
|
|
158
|
|
|
159 Global => null,
|
|
|
160 Post =>
|
|
|
161 Is_Singleton'Result =
|
|
|
162 (for all Item of Container => Equivalent_Elements (Item, New_Item));
|
|
|
163
|
|
|
164 function Not_In_Both
|
|
|
165 (Container : Set;
|
|
|
166 Left : Set;
|
|
|
167 Right : Set) return Boolean
|
|
|
168 -- Return True if there are no elements in Container that are in Left and
|
|
|
169 -- Right.
|
|
|
170
|
|
|
171 with
|
|
|
172 Global => null,
|
|
|
173 Post =>
|
|
|
174 Not_In_Both'Result =
|
|
|
175 (for all Item of Container =>
|
|
|
176 not Contains (Left, Item) or not Contains (Right, Item));
|
|
|
177
|
|
|
178 function No_Overlap (Left : Set; Right : Set) return Boolean with
|
|
|
179 -- Return True if there are no equivalent elements in Left and Right
|
|
|
180
|
|
|
181 Global => null,
|
|
|
182 Post =>
|
|
|
183 No_Overlap'Result =
|
|
|
184 (for all Item of Left => not Contains (Right, Item));
|
|
|
185
|
|
|
186 function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
|
|
|
187 -- Number of elements that are both in Left and Right
|
|
|
188
|
|
|
189 Global => null,
|
|
|
190 Post =>
|
|
|
191 Num_Overlaps'Result = Length (Intersection (Left, Right))
|
|
|
192 and (if Left <= Right then Num_Overlaps'Result = Length (Left)
|
|
|
193 else Num_Overlaps'Result < Length (Left))
|
|
|
194 and (if Right <= Left then Num_Overlaps'Result = Length (Right)
|
|
|
195 else Num_Overlaps'Result < Length (Right))
|
|
|
196 and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right);
|
|
|
197
|
|
|
198 ----------------------------
|
|
|
199 -- Construction Functions --
|
|
|
200 ----------------------------
|
|
|
201
|
|
|
202 -- For better efficiency of both proofs and execution, avoid using
|
|
|
203 -- construction functions in annotations and rather use property functions.
|
|
|
204
|
|
|
205 function Add (Container : Set; Item : Element_Type) return Set with
|
|
|
206 -- Return a new set containing all the elements of Container plus E
|
|
|
207
|
|
|
208 Global => null,
|
|
|
209 Pre =>
|
|
|
210 not Contains (Container, Item)
|
|
|
211 and Length (Container) < Count_Type'Last,
|
|
|
212 Post =>
|
|
|
213 Length (Add'Result) = Length (Container) + 1
|
|
|
214 and Contains (Add'Result, Item)
|
|
|
215 and Container <= Add'Result
|
|
|
216 and Included_Except (Add'Result, Container, Item);
|
|
|
217
|
|
|
218 function Remove (Container : Set; Item : Element_Type) return Set with
|
|
|
219 -- Return a new set containing all the elements of Container except E
|
|
|
220
|
|
|
221 Global => null,
|
|
|
222 Pre => Contains (Container, Item),
|
|
|
223 Post =>
|
|
|
224 Length (Remove'Result) = Length (Container) - 1
|
|
|
225 and not Contains (Remove'Result, Item)
|
|
|
226 and Remove'Result <= Container
|
|
|
227 and Included_Except (Container, Remove'Result, Item);
|
|
|
228
|
|
|
229 function Intersection (Left : Set; Right : Set) return Set with
|
|
|
230 -- Returns the intersection of Left and Right
|
|
|
231
|
|
|
232 Global => null,
|
|
|
233 Post =>
|
|
|
234 Intersection'Result <= Left
|
|
|
235 and Intersection'Result <= Right
|
|
|
236 and Includes_Intersection (Intersection'Result, Left, Right);
|
|
|
237
|
|
|
238 function Union (Left : Set; Right : Set) return Set with
|
|
|
239 -- Returns the union of Left and Right
|
|
|
240
|
|
|
241 Global => null,
|
|
|
242 Pre =>
|
|
|
243 Length (Left) - Num_Overlaps (Left, Right) <=
|
|
|
244 Count_Type'Last - Length (Right),
|
|
|
245 Post =>
|
|
|
246 Length (Union'Result) =
|
|
|
247 Length (Left) - Num_Overlaps (Left, Right) + Length (Right)
|
|
|
248 and Left <= Union'Result
|
|
|
249 and Right <= Union'Result
|
|
|
250 and Included_In_Union (Union'Result, Left, Right);
|
|
|
251
|
|
|
252 ---------------------------
|
|
|
253 -- Iteration Primitives --
|
|
|
254 ---------------------------
|
|
|
255
|
|
|
256 type Private_Key is private;
|
|
|
257
|
|
|
258 function Iter_First (Container : Set) return Private_Key with
|
|
|
259 Global => null;
|
|
|
260
|
|
|
261 function Iter_Has_Element
|
|
|
262 (Container : Set;
|
|
|
263 Key : Private_Key) return Boolean
|
|
|
264 with
|
|
|
265 Global => null;
|
|
|
266
|
|
|
267 function Iter_Next
|
|
|
268 (Container : Set;
|
|
|
269 Key : Private_Key) return Private_Key
|
|
|
270 with
|
|
|
271 Global => null,
|
|
|
272 Pre => Iter_Has_Element (Container, Key);
|
|
|
273
|
|
|
274 function Iter_Element
|
|
|
275 (Container : Set;
|
|
|
276 Key : Private_Key) return Element_Type
|
|
|
277 with
|
|
|
278 Global => null,
|
|
|
279 Pre => Iter_Has_Element (Container, Key);
|
|
|
280 pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains);
|
|
|
281
|
|
|
282 private
|
|
|
283
|
|
|
284 pragma SPARK_Mode (Off);
|
|
|
285
|
|
|
286 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
|
|
|
287
|
|
|
288 function "="
|
|
|
289 (Left : Element_Type;
|
|
|
290 Right : Element_Type) return Boolean renames Equivalent_Elements;
|
|
|
291
|
|
|
292 package Containers is new Ada.Containers.Functional_Base
|
|
|
293 (Element_Type => Element_Type,
|
|
|
294 Index_Type => Positive_Count_Type);
|
|
|
295
|
|
|
296 type Set is record
|
|
|
297 Content : Containers.Container;
|
|
|
298 end record;
|
|
|
299
|
|
|
300 type Private_Key is new Count_Type;
|
|
|
301
|
|
|
302 function Iter_First (Container : Set) return Private_Key is (1);
|
|
|
303
|
|
|
304 function Iter_Has_Element
|
|
|
305 (Container : Set;
|
|
|
306 Key : Private_Key) return Boolean
|
|
|
307 is
|
|
|
308 (Count_Type (Key) in 1 .. Containers.Length (Container.Content));
|
|
|
309
|
|
|
310 function Iter_Next
|
|
|
311 (Container : Set;
|
|
|
312 Key : Private_Key) return Private_Key
|
|
|
313 is
|
|
|
314 (if Key = Private_Key'Last then 0 else Key + 1);
|
|
|
315
|
|
|
316 function Iter_Element
|
|
|
317 (Container : Set;
|
|
|
318 Key : Private_Key) return Element_Type
|
|
|
319 is
|
|
|
320 (Containers.Get (Container.Content, Count_Type (Key)));
|
|
|
321
|
|
|
322 end Ada.Containers.Functional_Sets;
|
