|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ S E T S --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
131
|
9 -- Copyright (C) 2004-2018, 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 -- This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in
|
|
|
33 -- the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
|
|
|
34 -- making it easier to express properties, and by making the specification of
|
|
|
35 -- this unit compatible with SPARK 2014. Note that the API of this unit may be
|
|
|
36 -- subject to incompatible changes as SPARK 2014 evolves.
|
|
|
37
|
|
|
38 -- The modifications are:
|
|
|
39
|
|
|
40 -- A parameter for the container is added to every function reading the
|
|
|
41 -- content of a container: Key, Element, Next, Query_Element, Previous,
|
|
|
42 -- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
|
|
|
43 -- need to have cursors which are valid on different containers (typically
|
|
|
44 -- a container C and its previous version C'Old) for expressing properties,
|
|
|
45 -- which is not possible if cursors encapsulate an access to the underlying
|
|
|
46 -- container. The operators "<" and ">" that could not be modified that way
|
|
|
47 -- have been removed.
|
|
|
48
|
|
|
49 with Ada.Containers.Functional_Maps;
|
|
|
50 with Ada.Containers.Functional_Sets;
|
|
|
51 with Ada.Containers.Functional_Vectors;
|
|
|
52 private with Ada.Containers.Red_Black_Trees;
|
|
|
53
|
|
|
54 generic
|
|
|
55 type Element_Type is private;
|
|
|
56
|
|
|
57 with function "<" (Left, Right : Element_Type) return Boolean is <>;
|
|
|
58
|
|
|
59 package Ada.Containers.Formal_Ordered_Sets with
|
|
|
60 SPARK_Mode
|
|
|
61 is
|
|
|
62 pragma Annotate (CodePeer, Skip_Analysis);
|
|
|
63
|
|
|
64 function Equivalent_Elements (Left, Right : Element_Type) return Boolean
|
|
|
65 with
|
|
|
66 Global => null,
|
|
|
67 Post =>
|
|
|
68 Equivalent_Elements'Result =
|
|
|
69 (not (Left < Right) and not (Right < Left));
|
|
|
70 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements);
|
|
|
71
|
|
|
72 type Set (Capacity : Count_Type) is private with
|
|
|
73 Iterable => (First => First,
|
|
|
74 Next => Next,
|
|
|
75 Has_Element => Has_Element,
|
|
|
76 Element => Element),
|
|
|
77 Default_Initial_Condition => Is_Empty (Set);
|
|
|
78 pragma Preelaborable_Initialization (Set);
|
|
|
79
|
|
|
80 type Cursor is record
|
|
|
81 Node : Count_Type;
|
|
|
82 end record;
|
|
|
83
|
|
|
84 No_Element : constant Cursor := (Node => 0);
|
|
|
85
|
|
|
86 function Length (Container : Set) return Count_Type with
|
|
|
87 Global => null,
|
|
|
88 Post => Length'Result <= Container.Capacity;
|
|
|
89
|
|
|
90 pragma Unevaluated_Use_Of_Old (Allow);
|
|
|
91
|
|
|
92 package Formal_Model with Ghost is
|
|
|
93 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
|
|
|
94
|
|
|
95 package M is new Ada.Containers.Functional_Sets
|
|
|
96 (Element_Type => Element_Type,
|
|
|
97 Equivalent_Elements => Equivalent_Elements);
|
|
|
98
|
|
|
99 function "="
|
|
|
100 (Left : M.Set;
|
|
|
101 Right : M.Set) return Boolean renames M."=";
|
|
|
102
|
|
|
103 function "<="
|
|
|
104 (Left : M.Set;
|
|
|
105 Right : M.Set) return Boolean renames M."<=";
|
|
|
106
|
|
|
107 package E is new Ada.Containers.Functional_Vectors
|
|
|
108 (Element_Type => Element_Type,
|
|
|
109 Index_Type => Positive_Count_Type);
|
|
|
110
|
|
|
111 function "="
|
|
|
112 (Left : E.Sequence;
|
|
|
113 Right : E.Sequence) return Boolean renames E."=";
|
|
|
114
|
|
|
115 function "<"
|
|
|
116 (Left : E.Sequence;
|
|
|
117 Right : E.Sequence) return Boolean renames E."<";
|
|
|
118
|
|
|
119 function "<="
|
|
|
120 (Left : E.Sequence;
|
|
|
121 Right : E.Sequence) return Boolean renames E."<=";
|
|
|
122
|
|
|
123 function E_Bigger_Than_Range
|
|
|
124 (Container : E.Sequence;
|
|
|
125 Fst : Positive_Count_Type;
|
|
|
126 Lst : Count_Type;
|
|
|
127 Item : Element_Type) return Boolean
|
|
|
128 with
|
|
|
129 Global => null,
|
|
|
130 Pre => Lst <= E.Length (Container),
|
|
|
131 Post =>
|
|
|
132 E_Bigger_Than_Range'Result =
|
|
|
133 (for all I in Fst .. Lst => E.Get (Container, I) < Item);
|
|
|
134 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
|
|
|
135
|
|
|
136 function E_Smaller_Than_Range
|
|
|
137 (Container : E.Sequence;
|
|
|
138 Fst : Positive_Count_Type;
|
|
|
139 Lst : Count_Type;
|
|
|
140 Item : Element_Type) return Boolean
|
|
|
141 with
|
|
|
142 Global => null,
|
|
|
143 Pre => Lst <= E.Length (Container),
|
|
|
144 Post =>
|
|
|
145 E_Smaller_Than_Range'Result =
|
|
|
146 (for all I in Fst .. Lst => Item < E.Get (Container, I));
|
|
|
147 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
|
|
|
148
|
|
|
149 function E_Is_Find
|
|
|
150 (Container : E.Sequence;
|
|
|
151 Item : Element_Type;
|
|
|
152 Position : Count_Type) return Boolean
|
|
|
153 with
|
|
|
154 Global => null,
|
|
|
155 Pre => Position - 1 <= E.Length (Container),
|
|
|
156 Post =>
|
|
|
157 E_Is_Find'Result =
|
|
|
158
|
|
|
159 ((if Position > 0 then
|
|
|
160 E_Bigger_Than_Range (Container, 1, Position - 1, Item))
|
|
|
161
|
|
|
162 and (if Position < E.Length (Container) then
|
|
|
163 E_Smaller_Than_Range
|
|
|
164 (Container,
|
|
|
165 Position + 1,
|
|
|
166 E.Length (Container),
|
|
|
167 Item)));
|
|
|
168 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
|
|
|
169
|
|
|
170 function Find
|
|
|
171 (Container : E.Sequence;
|
|
|
172 Item : Element_Type) return Count_Type
|
|
|
173 -- Search for Item in Container
|
|
|
174
|
|
|
175 with
|
|
|
176 Global => null,
|
|
|
177 Post =>
|
|
|
178 (if Find'Result > 0 then
|
|
|
179 Find'Result <= E.Length (Container)
|
|
|
180 and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
|
|
|
181
|
|
|
182 function E_Elements_Included
|
|
|
183 (Left : E.Sequence;
|
|
|
184 Right : E.Sequence) return Boolean
|
|
|
185 -- The elements of Left are contained in Right
|
|
|
186
|
|
|
187 with
|
|
|
188 Global => null,
|
|
|
189 Post =>
|
|
|
190 E_Elements_Included'Result =
|
|
|
191 (for all I in 1 .. E.Length (Left) =>
|
|
|
192 Find (Right, E.Get (Left, I)) > 0
|
|
|
193 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
|
|
|
194 E.Get (Left, I));
|
|
|
195 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
196
|
|
|
197 function E_Elements_Included
|
|
|
198 (Left : E.Sequence;
|
|
|
199 Model : M.Set;
|
|
|
200 Right : E.Sequence) return Boolean
|
|
|
201 -- The elements of Container contained in Model are in Right
|
|
|
202
|
|
|
203 with
|
|
|
204 Global => null,
|
|
|
205 Post =>
|
|
|
206 E_Elements_Included'Result =
|
|
|
207 (for all I in 1 .. E.Length (Left) =>
|
|
|
208 (if M.Contains (Model, E.Get (Left, I)) then
|
|
|
209 Find (Right, E.Get (Left, I)) > 0
|
|
|
210 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
|
|
|
211 E.Get (Left, I)));
|
|
|
212 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
213
|
|
|
214 function E_Elements_Included
|
|
|
215 (Container : E.Sequence;
|
|
|
216 Model : M.Set;
|
|
|
217 Left : E.Sequence;
|
|
|
218 Right : E.Sequence) return Boolean
|
|
|
219 -- The elements of Container contained in Model are in Left and others
|
|
|
220 -- are in Right.
|
|
|
221
|
|
|
222 with
|
|
|
223 Global => null,
|
|
|
224 Post =>
|
|
|
225 E_Elements_Included'Result =
|
|
|
226 (for all I in 1 .. E.Length (Container) =>
|
|
|
227 (if M.Contains (Model, E.Get (Container, I)) then
|
|
|
228 Find (Left, E.Get (Container, I)) > 0
|
|
|
229 and then E.Get (Left, Find (Left, E.Get (Container, I))) =
|
|
|
230 E.Get (Container, I)
|
|
|
231 else
|
|
|
232 Find (Right, E.Get (Container, I)) > 0
|
|
|
233 and then E.Get (Right, Find (Right, E.Get (Container, I))) =
|
|
|
234 E.Get (Container, I)));
|
|
|
235 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
236
|
|
|
237 package P is new Ada.Containers.Functional_Maps
|
|
|
238 (Key_Type => Cursor,
|
|
|
239 Element_Type => Positive_Count_Type,
|
|
|
240 Equivalent_Keys => "=",
|
|
|
241 Enable_Handling_Of_Equivalence => False);
|
|
|
242
|
|
|
243 function "="
|
|
|
244 (Left : P.Map;
|
|
|
245 Right : P.Map) return Boolean renames P."=";
|
|
|
246
|
|
|
247 function "<="
|
|
|
248 (Left : P.Map;
|
|
|
249 Right : P.Map) return Boolean renames P."<=";
|
|
|
250
|
|
|
251 function P_Positions_Shifted
|
|
|
252 (Small : P.Map;
|
|
|
253 Big : P.Map;
|
|
|
254 Cut : Positive_Count_Type;
|
|
|
255 Count : Count_Type := 1) return Boolean
|
|
|
256 with
|
|
|
257 Global => null,
|
|
|
258 Post =>
|
|
|
259 P_Positions_Shifted'Result =
|
|
|
260
|
|
|
261 -- Big contains all cursors of Small
|
|
|
262
|
|
|
263 (P.Keys_Included (Small, Big)
|
|
|
264
|
|
|
265 -- Cursors located before Cut are not moved, cursors located
|
|
|
266 -- after are shifted by Count.
|
|
|
267
|
|
|
268 and (for all I of Small =>
|
|
|
269 (if P.Get (Small, I) < Cut then
|
|
|
270 P.Get (Big, I) = P.Get (Small, I)
|
|
|
271 else
|
|
|
272 P.Get (Big, I) - Count = P.Get (Small, I)))
|
|
|
273
|
|
|
274 -- New cursors of Big (if any) are between Cut and Cut - 1 +
|
|
|
275 -- Count.
|
|
|
276
|
|
|
277 and (for all I of Big =>
|
|
|
278 P.Has_Key (Small, I)
|
|
|
279 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
|
|
|
280
|
|
|
281 function Mapping_Preserved
|
|
|
282 (E_Left : E.Sequence;
|
|
|
283 E_Right : E.Sequence;
|
|
|
284 P_Left : P.Map;
|
|
|
285 P_Right : P.Map) return Boolean
|
|
|
286 with
|
|
|
287 Ghost,
|
|
|
288 Global => null,
|
|
|
289 Post =>
|
|
|
290 (if Mapping_Preserved'Result then
|
|
|
291
|
|
|
292 -- Right contains all the cursors of Left
|
|
|
293
|
|
|
294 P.Keys_Included (P_Left, P_Right)
|
|
|
295
|
|
|
296 -- Right contains all the elements of Left
|
|
|
297
|
|
|
298 and E_Elements_Included (E_Left, E_Right)
|
|
|
299
|
|
|
300 -- Mappings from cursors to elements induced by E_Left, P_Left
|
|
|
301 -- and E_Right, P_Right are the same.
|
|
|
302
|
|
|
303 and (for all C of P_Left =>
|
|
|
304 E.Get (E_Left, P.Get (P_Left, C)) =
|
|
|
305 E.Get (E_Right, P.Get (P_Right, C))));
|
|
|
306
|
|
|
307 function Mapping_Preserved_Except
|
|
|
308 (E_Left : E.Sequence;
|
|
|
309 E_Right : E.Sequence;
|
|
|
310 P_Left : P.Map;
|
|
|
311 P_Right : P.Map;
|
|
|
312 Position : Cursor) return Boolean
|
|
|
313 with
|
|
|
314 Ghost,
|
|
|
315 Global => null,
|
|
|
316 Post =>
|
|
|
317 (if Mapping_Preserved_Except'Result then
|
|
|
318
|
|
|
319 -- Right contains all the cursors of Left
|
|
|
320
|
|
|
321 P.Keys_Included (P_Left, P_Right)
|
|
|
322
|
|
|
323 -- Mappings from cursors to elements induced by E_Left, P_Left
|
|
|
324 -- and E_Right, P_Right are the same except for Position.
|
|
|
325
|
|
|
326 and (for all C of P_Left =>
|
|
|
327 (if C /= Position then
|
|
|
328 E.Get (E_Left, P.Get (P_Left, C)) =
|
|
|
329 E.Get (E_Right, P.Get (P_Right, C)))));
|
|
|
330
|
|
|
331 function Model (Container : Set) return M.Set with
|
|
|
332 -- The high-level model of a set is a set of elements. Neither cursors
|
|
|
333 -- nor order of elements are represented in this model. Elements are
|
|
|
334 -- modeled up to equivalence.
|
|
|
335
|
|
|
336 Ghost,
|
|
|
337 Global => null,
|
|
|
338 Post => M.Length (Model'Result) = Length (Container);
|
|
|
339
|
|
|
340 function Elements (Container : Set) return E.Sequence with
|
|
|
341 -- The Elements sequence represents the underlying list structure of
|
|
|
342 -- sets that is used for iteration. It stores the actual values of
|
|
|
343 -- elements in the set. It does not model cursors.
|
|
|
344
|
|
|
345 Ghost,
|
|
|
346 Global => null,
|
|
|
347 Post =>
|
|
|
348 E.Length (Elements'Result) = Length (Container)
|
|
|
349
|
|
|
350 -- It only contains keys contained in Model
|
|
|
351
|
|
|
352 and (for all Item of Elements'Result =>
|
|
|
353 M.Contains (Model (Container), Item))
|
|
|
354
|
|
|
355 -- It contains all the elements contained in Model
|
|
|
356
|
|
|
357 and (for all Item of Model (Container) =>
|
|
|
358 (Find (Elements'Result, Item) > 0
|
|
|
359 and then Equivalent_Elements
|
|
|
360 (E.Get (Elements'Result, Find (Elements'Result, Item)),
|
|
|
361 Item)))
|
|
|
362
|
|
|
363 -- It is sorted in increasing order
|
|
|
364
|
|
|
365 and (for all I in 1 .. Length (Container) =>
|
|
|
366 Find (Elements'Result, E.Get (Elements'Result, I)) = I
|
|
|
367 and
|
|
|
368 E_Is_Find
|
|
|
369 (Elements'Result, E.Get (Elements'Result, I), I));
|
|
|
370 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
|
|
|
371
|
|
|
372 function Positions (Container : Set) return P.Map with
|
|
|
373 -- The Positions map is used to model cursors. It only contains valid
|
|
|
374 -- cursors and maps them to their position in the container.
|
|
|
375
|
|
|
376 Ghost,
|
|
|
377 Global => null,
|
|
|
378 Post =>
|
|
|
379 not P.Has_Key (Positions'Result, No_Element)
|
|
|
380
|
|
|
381 -- Positions of cursors are smaller than the container's length
|
|
|
382
|
|
|
383 and then
|
|
|
384 (for all I of Positions'Result =>
|
|
|
385 P.Get (Positions'Result, I) in 1 .. Length (Container)
|
|
|
386
|
|
|
387 -- No two cursors have the same position. Note that we do not
|
|
|
388 -- state that there is a cursor in the map for each position, as
|
|
|
389 -- it is rarely needed.
|
|
|
390
|
|
|
391 and then
|
|
|
392 (for all J of Positions'Result =>
|
|
|
393 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
|
|
|
394 then I = J)));
|
|
|
395
|
|
|
396 procedure Lift_Abstraction_Level (Container : Set) with
|
|
|
397 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
|
|
|
398 -- assume that we can access the same elements by iterating over
|
|
|
399 -- positions or cursors.
|
|
|
400 -- This information is not generally useful except when switching from
|
|
|
401 -- a low-level, cursor-aware view of a container, to a high-level,
|
|
|
402 -- position-based view.
|
|
|
403
|
|
|
404 Ghost,
|
|
|
405 Global => null,
|
|
|
406 Post =>
|
|
|
407 (for all Item of Elements (Container) =>
|
|
|
408 (for some I of Positions (Container) =>
|
|
|
409 E.Get (Elements (Container), P.Get (Positions (Container), I)) =
|
|
|
410 Item));
|
|
|
411
|
|
|
412 function Contains
|
|
|
413 (C : M.Set;
|
|
|
414 K : Element_Type) return Boolean renames M.Contains;
|
|
|
415 -- To improve readability of contracts, we rename the function used to
|
|
|
416 -- search for an element in the model to Contains.
|
|
|
417
|
|
|
418 end Formal_Model;
|
|
|
419 use Formal_Model;
|
|
|
420
|
|
|
421 Empty_Set : constant Set;
|
|
|
422
|
|
|
423 function "=" (Left, Right : Set) return Boolean with
|
|
|
424 Global => null,
|
|
|
425 Post =>
|
|
|
426
|
|
|
427 -- If two sets are equal, they contain the same elements in the same
|
|
|
428 -- order.
|
|
|
429
|
|
|
430 (if "="'Result then Elements (Left) = Elements (Right)
|
|
|
431
|
|
|
432 -- If they are different, then they do not contain the same elements
|
|
|
433
|
|
|
434 else
|
|
|
435 not E_Elements_Included (Elements (Left), Elements (Right))
|
|
|
436 or not E_Elements_Included (Elements (Right), Elements (Left)));
|
|
|
437
|
|
|
438 function Equivalent_Sets (Left, Right : Set) return Boolean with
|
|
|
439 Global => null,
|
|
|
440 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
|
|
|
441
|
|
|
442 function To_Set (New_Item : Element_Type) return Set with
|
|
|
443 Global => null,
|
|
|
444 Post =>
|
|
|
445 M.Is_Singleton (Model (To_Set'Result), New_Item)
|
|
|
446 and Length (To_Set'Result) = 1
|
|
|
447 and E.Get (Elements (To_Set'Result), 1) = New_Item;
|
|
|
448
|
|
|
449 function Is_Empty (Container : Set) return Boolean with
|
|
|
450 Global => null,
|
|
|
451 Post => Is_Empty'Result = (Length (Container) = 0);
|
|
|
452
|
|
|
453 procedure Clear (Container : in out Set) with
|
|
|
454 Global => null,
|
|
|
455 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
|
|
|
456
|
|
|
457 procedure Assign (Target : in out Set; Source : Set) with
|
|
|
458 Global => null,
|
|
|
459 Pre => Target.Capacity >= Length (Source),
|
|
|
460 Post =>
|
|
|
461 Model (Target) = Model (Source)
|
|
|
462 and Elements (Target) = Elements (Source)
|
|
|
463 and Length (Target) = Length (Source);
|
|
|
464
|
|
|
465 function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
|
|
|
466 Global => null,
|
|
|
467 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
|
|
|
468 Post =>
|
|
|
469 Model (Copy'Result) = Model (Source)
|
|
|
470 and Elements (Copy'Result) = Elements (Source)
|
|
|
471 and Positions (Copy'Result) = Positions (Source)
|
|
|
472 and (if Capacity = 0 then
|
|
|
473 Copy'Result.Capacity = Source.Capacity
|
|
|
474 else
|
|
|
475 Copy'Result.Capacity = Capacity);
|
|
|
476
|
|
|
477 function Element
|
|
|
478 (Container : Set;
|
|
|
479 Position : Cursor) return Element_Type
|
|
|
480 with
|
|
|
481 Global => null,
|
|
|
482 Pre => Has_Element (Container, Position),
|
|
|
483 Post =>
|
|
|
484 Element'Result =
|
|
|
485 E.Get (Elements (Container), P.Get (Positions (Container), Position));
|
|
|
486 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
487
|
|
|
488 procedure Replace_Element
|
|
|
489 (Container : in out Set;
|
|
|
490 Position : Cursor;
|
|
|
491 New_Item : Element_Type)
|
|
|
492 with
|
|
|
493 Global => null,
|
|
|
494 Pre => Has_Element (Container, Position),
|
|
|
495 Post =>
|
|
|
496 Length (Container) = Length (Container)'Old
|
|
|
497
|
|
|
498 -- Position now maps to New_Item
|
|
|
499
|
|
|
500 and Element (Container, Position) = New_Item
|
|
|
501
|
|
|
502 -- New_Item is contained in Container
|
|
|
503
|
|
|
504 and Contains (Model (Container), New_Item)
|
|
|
505
|
|
|
506 -- Other elements are preserved
|
|
|
507
|
|
|
508 and M.Included_Except
|
|
|
509 (Model (Container)'Old,
|
|
|
510 Model (Container),
|
|
|
511 Element (Container, Position)'Old)
|
|
|
512 and M.Included_Except
|
|
|
513 (Model (Container),
|
|
|
514 Model (Container)'Old,
|
|
|
515 New_Item)
|
|
|
516
|
|
|
517 -- Mapping from cursors to elements is preserved
|
|
|
518
|
|
|
519 and Mapping_Preserved_Except
|
|
|
520 (E_Left => Elements (Container)'Old,
|
|
|
521 E_Right => Elements (Container),
|
|
|
522 P_Left => Positions (Container)'Old,
|
|
|
523 P_Right => Positions (Container),
|
|
|
524 Position => Position)
|
|
|
525 and Positions (Container) = Positions (Container)'Old;
|
|
|
526
|
|
|
527 procedure Move (Target : in out Set; Source : in out Set) with
|
|
|
528 Global => null,
|
|
|
529 Pre => Target.Capacity >= Length (Source),
|
|
|
530 Post =>
|
|
|
531 Model (Target) = Model (Source)'Old
|
|
|
532 and Elements (Target) = Elements (Source)'Old
|
|
|
533 and Length (Source)'Old = Length (Target)
|
|
|
534 and Length (Source) = 0;
|
|
|
535
|
|
|
536 procedure Insert
|
|
|
537 (Container : in out Set;
|
|
|
538 New_Item : Element_Type;
|
|
|
539 Position : out Cursor;
|
|
|
540 Inserted : out Boolean)
|
|
|
541 with
|
|
|
542 Global => null,
|
|
|
543 Pre =>
|
|
|
544 Length (Container) < Container.Capacity
|
|
|
545 or Contains (Container, New_Item),
|
|
|
546 Post =>
|
|
|
547 Contains (Container, New_Item)
|
|
|
548 and Has_Element (Container, Position)
|
|
|
549 and Equivalent_Elements (Element (Container, Position), New_Item)
|
|
|
550 and E_Is_Find
|
|
|
551 (Elements (Container),
|
|
|
552 New_Item,
|
|
|
553 P.Get (Positions (Container), Position)),
|
|
|
554 Contract_Cases =>
|
|
|
555
|
|
|
556 -- If New_Item is already in Container, it is not modified and Inserted
|
|
|
557 -- is set to False.
|
|
|
558
|
|
|
559 (Contains (Container, New_Item) =>
|
|
|
560 not Inserted
|
|
|
561 and Model (Container) = Model (Container)'Old
|
|
|
562 and Elements (Container) = Elements (Container)'Old
|
|
|
563 and Positions (Container) = Positions (Container)'Old,
|
|
|
564
|
|
|
565 -- Otherwise, New_Item is inserted in Container and Inserted is set to
|
|
|
566 -- True
|
|
|
567
|
|
|
568 others =>
|
|
|
569 Inserted
|
|
|
570 and Length (Container) = Length (Container)'Old + 1
|
|
|
571
|
|
|
572 -- Position now maps to New_Item
|
|
|
573
|
|
|
574 and Element (Container, Position) = New_Item
|
|
|
575
|
|
|
576 -- Other elements are preserved
|
|
|
577
|
|
|
578 and Model (Container)'Old <= Model (Container)
|
|
|
579 and M.Included_Except
|
|
|
580 (Model (Container),
|
|
|
581 Model (Container)'Old,
|
|
|
582 New_Item)
|
|
|
583
|
|
|
584 -- The elements of Container located before Position are preserved
|
|
|
585
|
|
|
586 and E.Range_Equal
|
|
|
587 (Left => Elements (Container)'Old,
|
|
|
588 Right => Elements (Container),
|
|
|
589 Fst => 1,
|
|
|
590 Lst => P.Get (Positions (Container), Position) - 1)
|
|
|
591
|
|
|
592 -- Other elements are shifted by 1
|
|
|
593
|
|
|
594 and E.Range_Shifted
|
|
|
595 (Left => Elements (Container)'Old,
|
|
|
596 Right => Elements (Container),
|
|
|
597 Fst => P.Get (Positions (Container), Position),
|
|
|
598 Lst => Length (Container)'Old,
|
|
|
599 Offset => 1)
|
|
|
600
|
|
|
601 -- A new cursor has been inserted at position Position in
|
|
|
602 -- Container.
|
|
|
603
|
|
|
604 and P_Positions_Shifted
|
|
|
605 (Positions (Container)'Old,
|
|
|
606 Positions (Container),
|
|
|
607 Cut => P.Get (Positions (Container), Position)));
|
|
|
608
|
|
|
609 procedure Insert
|
|
|
610 (Container : in out Set;
|
|
|
611 New_Item : Element_Type)
|
|
|
612 with
|
|
|
613 Global => null,
|
|
|
614 Pre =>
|
|
|
615 Length (Container) < Container.Capacity
|
|
|
616 and then (not Contains (Container, New_Item)),
|
|
|
617 Post =>
|
|
|
618 Length (Container) = Length (Container)'Old + 1
|
|
|
619 and Contains (Container, New_Item)
|
|
|
620
|
|
|
621 -- New_Item is inserted in the set
|
|
|
622
|
|
|
623 and E.Get (Elements (Container),
|
|
|
624 Find (Elements (Container), New_Item)) = New_Item
|
|
|
625
|
|
|
626 -- Other mappings are preserved
|
|
|
627
|
|
|
628 and Model (Container)'Old <= Model (Container)
|
|
|
629 and M.Included_Except
|
|
|
630 (Model (Container),
|
|
|
631 Model (Container)'Old,
|
|
|
632 New_Item)
|
|
|
633
|
|
|
634 -- The elements of Container located before New_Item are preserved
|
|
|
635
|
|
|
636 and E.Range_Equal
|
|
|
637 (Left => Elements (Container)'Old,
|
|
|
638 Right => Elements (Container),
|
|
|
639 Fst => 1,
|
|
|
640 Lst => Find (Elements (Container), New_Item) - 1)
|
|
|
641
|
|
|
642 -- Other elements are shifted by 1
|
|
|
643
|
|
|
644 and E.Range_Shifted
|
|
|
645 (Left => Elements (Container)'Old,
|
|
|
646 Right => Elements (Container),
|
|
|
647 Fst => Find (Elements (Container), New_Item),
|
|
|
648 Lst => Length (Container)'Old,
|
|
|
649 Offset => 1)
|
|
|
650
|
|
|
651 -- A new cursor has been inserted in Container
|
|
|
652
|
|
|
653 and P_Positions_Shifted
|
|
|
654 (Positions (Container)'Old,
|
|
|
655 Positions (Container),
|
|
|
656 Cut => Find (Elements (Container), New_Item));
|
|
|
657
|
|
|
658 procedure Include
|
|
|
659 (Container : in out Set;
|
|
|
660 New_Item : Element_Type)
|
|
|
661 with
|
|
|
662 Global => null,
|
|
|
663 Pre =>
|
|
|
664 Length (Container) < Container.Capacity
|
|
|
665 or Contains (Container, New_Item),
|
|
|
666 Post => Contains (Container, New_Item),
|
|
|
667 Contract_Cases =>
|
|
|
668
|
|
|
669 -- If New_Item is already in Container
|
|
|
670
|
|
|
671 (Contains (Container, New_Item) =>
|
|
|
672
|
|
|
673 -- Elements are preserved
|
|
|
674
|
|
|
675 Model (Container)'Old = Model (Container)
|
|
|
676
|
|
|
677 -- Cursors are preserved
|
|
|
678
|
|
|
679 and Positions (Container) = Positions (Container)'Old
|
|
|
680
|
|
|
681 -- The element equivalent to New_Item in Container is replaced by
|
|
|
682 -- New_Item.
|
|
|
683
|
|
|
684 and E.Get (Elements (Container),
|
|
|
685 Find (Elements (Container), New_Item)) = New_Item
|
|
|
686
|
|
|
687 and E.Equal_Except
|
|
|
688 (Elements (Container)'Old,
|
|
|
689 Elements (Container),
|
|
|
690 Find (Elements (Container), New_Item)),
|
|
|
691
|
|
|
692 -- Otherwise, New_Item is inserted in Container
|
|
|
693
|
|
|
694 others =>
|
|
|
695 Length (Container) = Length (Container)'Old + 1
|
|
|
696
|
|
|
697 -- Other elements are preserved
|
|
|
698
|
|
|
699 and Model (Container)'Old <= Model (Container)
|
|
|
700 and M.Included_Except
|
|
|
701 (Model (Container),
|
|
|
702 Model (Container)'Old,
|
|
|
703 New_Item)
|
|
|
704
|
|
|
705 -- New_Item is inserted in Container
|
|
|
706
|
|
|
707 and E.Get (Elements (Container),
|
|
|
708 Find (Elements (Container), New_Item)) = New_Item
|
|
|
709
|
|
|
710 -- The Elements of Container located before New_Item are preserved
|
|
|
711
|
|
|
712 and E.Range_Equal
|
|
|
713 (Left => Elements (Container)'Old,
|
|
|
714 Right => Elements (Container),
|
|
|
715 Fst => 1,
|
|
|
716 Lst => Find (Elements (Container), New_Item) - 1)
|
|
|
717
|
|
|
718 -- Other Elements are shifted by 1
|
|
|
719
|
|
|
720 and E.Range_Shifted
|
|
|
721 (Left => Elements (Container)'Old,
|
|
|
722 Right => Elements (Container),
|
|
|
723 Fst => Find (Elements (Container), New_Item),
|
|
|
724 Lst => Length (Container)'Old,
|
|
|
725 Offset => 1)
|
|
|
726
|
|
|
727 -- A new cursor has been inserted in Container
|
|
|
728
|
|
|
729 and P_Positions_Shifted
|
|
|
730 (Positions (Container)'Old,
|
|
|
731 Positions (Container),
|
|
|
732 Cut => Find (Elements (Container), New_Item)));
|
|
|
733
|
|
|
734 procedure Replace
|
|
|
735 (Container : in out Set;
|
|
|
736 New_Item : Element_Type)
|
|
|
737 with
|
|
|
738 Global => null,
|
|
|
739 Pre => Contains (Container, New_Item),
|
|
|
740 Post =>
|
|
|
741
|
|
|
742 -- Elements are preserved
|
|
|
743
|
|
|
744 Model (Container)'Old = Model (Container)
|
|
|
745
|
|
|
746 -- Cursors are preserved
|
|
|
747
|
|
|
748 and Positions (Container) = Positions (Container)'Old
|
|
|
749
|
|
|
750 -- The element equivalent to New_Item in Container is replaced by
|
|
|
751 -- New_Item.
|
|
|
752
|
|
|
753 and E.Get (Elements (Container),
|
|
|
754 Find (Elements (Container), New_Item)) = New_Item
|
|
|
755 and E.Equal_Except
|
|
|
756 (Elements (Container)'Old,
|
|
|
757 Elements (Container),
|
|
|
758 Find (Elements (Container), New_Item));
|
|
|
759
|
|
|
760 procedure Exclude
|
|
|
761 (Container : in out Set;
|
|
|
762 Item : Element_Type)
|
|
|
763 with
|
|
|
764 Global => null,
|
|
|
765 Post => not Contains (Container, Item),
|
|
|
766 Contract_Cases =>
|
|
|
767
|
|
|
768 -- If Item is not in Container, nothing is changed
|
|
|
769
|
|
|
770 (not Contains (Container, Item) =>
|
|
|
771 Model (Container) = Model (Container)'Old
|
|
|
772 and Elements (Container) = Elements (Container)'Old
|
|
|
773 and Positions (Container) = Positions (Container)'Old,
|
|
|
774
|
|
|
775 -- Otherwise, Item is removed from Container
|
|
|
776
|
|
|
777 others =>
|
|
|
778 Length (Container) = Length (Container)'Old - 1
|
|
|
779
|
|
|
780 -- Other elements are preserved
|
|
|
781
|
|
|
782 and Model (Container) <= Model (Container)'Old
|
|
|
783 and M.Included_Except
|
|
|
784 (Model (Container)'Old,
|
|
|
785 Model (Container),
|
|
|
786 Item)
|
|
|
787
|
|
|
788 -- The elements of Container located before Item are preserved
|
|
|
789
|
|
|
790 and E.Range_Equal
|
|
|
791 (Left => Elements (Container)'Old,
|
|
|
792 Right => Elements (Container),
|
|
|
793 Fst => 1,
|
|
|
794 Lst => Find (Elements (Container), Item)'Old - 1)
|
|
|
795
|
|
|
796 -- The elements located after Item are shifted by 1
|
|
|
797
|
|
|
798 and E.Range_Shifted
|
|
|
799 (Left => Elements (Container),
|
|
|
800 Right => Elements (Container)'Old,
|
|
|
801 Fst => Find (Elements (Container), Item)'Old,
|
|
|
802 Lst => Length (Container),
|
|
|
803 Offset => 1)
|
|
|
804
|
|
|
805 -- A cursor has been removed from Container
|
|
|
806
|
|
|
807 and P_Positions_Shifted
|
|
|
808 (Positions (Container),
|
|
|
809 Positions (Container)'Old,
|
|
|
810 Cut => Find (Elements (Container), Item)'Old));
|
|
|
811
|
|
|
812 procedure Delete
|
|
|
813 (Container : in out Set;
|
|
|
814 Item : Element_Type)
|
|
|
815 with
|
|
|
816 Global => null,
|
|
|
817 Pre => Contains (Container, Item),
|
|
|
818 Post =>
|
|
|
819 Length (Container) = Length (Container)'Old - 1
|
|
|
820
|
|
|
821 -- Item is no longer in Container
|
|
|
822
|
|
|
823 and not Contains (Container, Item)
|
|
|
824
|
|
|
825 -- Other elements are preserved
|
|
|
826
|
|
|
827 and Model (Container) <= Model (Container)'Old
|
|
|
828 and M.Included_Except
|
|
|
829 (Model (Container)'Old,
|
|
|
830 Model (Container),
|
|
|
831 Item)
|
|
|
832
|
|
|
833 -- The elements of Container located before Item are preserved
|
|
|
834
|
|
|
835 and E.Range_Equal
|
|
|
836 (Left => Elements (Container)'Old,
|
|
|
837 Right => Elements (Container),
|
|
|
838 Fst => 1,
|
|
|
839 Lst => Find (Elements (Container), Item)'Old - 1)
|
|
|
840
|
|
|
841 -- The elements located after Item are shifted by 1
|
|
|
842
|
|
|
843 and E.Range_Shifted
|
|
|
844 (Left => Elements (Container),
|
|
|
845 Right => Elements (Container)'Old,
|
|
|
846 Fst => Find (Elements (Container), Item)'Old,
|
|
|
847 Lst => Length (Container),
|
|
|
848 Offset => 1)
|
|
|
849
|
|
|
850 -- A cursor has been removed from Container
|
|
|
851
|
|
|
852 and P_Positions_Shifted
|
|
|
853 (Positions (Container),
|
|
|
854 Positions (Container)'Old,
|
|
|
855 Cut => Find (Elements (Container), Item)'Old);
|
|
|
856
|
|
|
857 procedure Delete
|
|
|
858 (Container : in out Set;
|
|
|
859 Position : in out Cursor)
|
|
|
860 with
|
|
|
861 Global => null,
|
|
|
862 Pre => Has_Element (Container, Position),
|
|
|
863 Post =>
|
|
|
864 Position = No_Element
|
|
|
865 and Length (Container) = Length (Container)'Old - 1
|
|
|
866
|
|
|
867 -- The element at position Position is no longer in Container
|
|
|
868
|
|
|
869 and not Contains (Container, Element (Container, Position)'Old)
|
|
|
870 and not P.Has_Key (Positions (Container), Position'Old)
|
|
|
871
|
|
|
872 -- Other elements are preserved
|
|
|
873
|
|
|
874 and Model (Container) <= Model (Container)'Old
|
|
|
875 and M.Included_Except
|
|
|
876 (Model (Container)'Old,
|
|
|
877 Model (Container),
|
|
|
878 Element (Container, Position)'Old)
|
|
|
879
|
|
|
880 -- The elements of Container located before Position are preserved.
|
|
|
881
|
|
|
882 and E.Range_Equal
|
|
|
883 (Left => Elements (Container)'Old,
|
|
|
884 Right => Elements (Container),
|
|
|
885 Fst => 1,
|
|
|
886 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
|
|
|
887
|
|
|
888 -- The elements located after Position are shifted by 1
|
|
|
889
|
|
|
890 and E.Range_Shifted
|
|
|
891 (Left => Elements (Container),
|
|
|
892 Right => Elements (Container)'Old,
|
|
|
893 Fst => P.Get (Positions (Container)'Old, Position'Old),
|
|
|
894 Lst => Length (Container),
|
|
|
895 Offset => 1)
|
|
|
896
|
|
|
897 -- Position has been removed from Container
|
|
|
898
|
|
|
899 and P_Positions_Shifted
|
|
|
900 (Positions (Container),
|
|
|
901 Positions (Container)'Old,
|
|
|
902 Cut => P.Get (Positions (Container)'Old, Position'Old));
|
|
|
903
|
|
|
904 procedure Delete_First (Container : in out Set) with
|
|
|
905 Global => null,
|
|
|
906 Contract_Cases =>
|
|
|
907 (Length (Container) = 0 => Length (Container) = 0,
|
|
|
908 others =>
|
|
|
909 Length (Container) = Length (Container)'Old - 1
|
|
|
910
|
|
|
911 -- The first element has been removed from Container
|
|
|
912
|
|
|
913 and not Contains (Container, First_Element (Container)'Old)
|
|
|
914
|
|
|
915 -- Other elements are preserved
|
|
|
916
|
|
|
917 and Model (Container) <= Model (Container)'Old
|
|
|
918 and M.Included_Except
|
|
|
919 (Model (Container)'Old,
|
|
|
920 Model (Container),
|
|
|
921 First_Element (Container)'Old)
|
|
|
922
|
|
|
923 -- Other elements are shifted by 1
|
|
|
924
|
|
|
925 and E.Range_Shifted
|
|
|
926 (Left => Elements (Container),
|
|
|
927 Right => Elements (Container)'Old,
|
|
|
928 Fst => 1,
|
|
|
929 Lst => Length (Container),
|
|
|
930 Offset => 1)
|
|
|
931
|
|
|
932 -- First has been removed from Container
|
|
|
933
|
|
|
934 and P_Positions_Shifted
|
|
|
935 (Positions (Container),
|
|
|
936 Positions (Container)'Old,
|
|
|
937 Cut => 1));
|
|
|
938
|
|
|
939 procedure Delete_Last (Container : in out Set) with
|
|
|
940 Global => null,
|
|
|
941 Contract_Cases =>
|
|
|
942 (Length (Container) = 0 => Length (Container) = 0,
|
|
|
943 others =>
|
|
|
944 Length (Container) = Length (Container)'Old - 1
|
|
|
945
|
|
|
946 -- The last element has been removed from Container
|
|
|
947
|
|
|
948 and not Contains (Container, Last_Element (Container)'Old)
|
|
|
949
|
|
|
950 -- Other elements are preserved
|
|
|
951
|
|
|
952 and Model (Container) <= Model (Container)'Old
|
|
|
953 and M.Included_Except
|
|
|
954 (Model (Container)'Old,
|
|
|
955 Model (Container),
|
|
|
956 Last_Element (Container)'Old)
|
|
|
957
|
|
|
958 -- Others elements of Container are preserved
|
|
|
959
|
|
|
960 and E.Range_Equal
|
|
|
961 (Left => Elements (Container)'Old,
|
|
|
962 Right => Elements (Container),
|
|
|
963 Fst => 1,
|
|
|
964 Lst => Length (Container))
|
|
|
965
|
|
|
966 -- Last cursor has been removed from Container
|
|
|
967
|
|
|
968 and Positions (Container) <= Positions (Container)'Old);
|
|
|
969
|
|
|
970 procedure Union (Target : in out Set; Source : Set) with
|
|
|
971 Global => null,
|
|
|
972 Pre =>
|
|
|
973 Length (Source) - Length (Target and Source) <=
|
|
|
974 Target.Capacity - Length (Target),
|
|
|
975 Post =>
|
|
|
976 Length (Target) = Length (Target)'Old
|
|
|
977 - M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
978 + Length (Source)
|
|
|
979
|
|
|
980 -- Elements already in Target are still in Target
|
|
|
981
|
|
|
982 and Model (Target)'Old <= Model (Target)
|
|
|
983
|
|
|
984 -- Elements of Source are included in Target
|
|
|
985
|
|
|
986 and Model (Source) <= Model (Target)
|
|
|
987
|
|
|
988 -- Elements of Target come from either Source or Target
|
|
|
989
|
|
|
990 and
|
|
|
991 M.Included_In_Union
|
|
|
992 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
993
|
|
|
994 -- Actual value of elements come from either Left or Right
|
|
|
995
|
|
|
996 and
|
|
|
997 E_Elements_Included
|
|
|
998 (Elements (Target),
|
|
|
999 Model (Target)'Old,
|
|
|
1000 Elements (Target)'Old,
|
|
|
1001 Elements (Source))
|
|
|
1002 and
|
|
|
1003 E_Elements_Included
|
|
|
1004 (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
|
|
|
1005 and
|
|
|
1006 E_Elements_Included
|
|
|
1007 (Elements (Source),
|
|
|
1008 Model (Target)'Old,
|
|
|
1009 Elements (Source),
|
|
|
1010 Elements (Target))
|
|
|
1011
|
|
|
1012 -- Mapping from cursors of Target to elements is preserved
|
|
|
1013
|
|
|
1014 and Mapping_Preserved
|
|
|
1015 (E_Left => Elements (Target)'Old,
|
|
|
1016 E_Right => Elements (Target),
|
|
|
1017 P_Left => Positions (Target)'Old,
|
|
|
1018 P_Right => Positions (Target));
|
|
|
1019
|
|
|
1020 function Union (Left, Right : Set) return Set with
|
|
|
1021 Global => null,
|
|
|
1022 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
1023 Post =>
|
|
|
1024 Length (Union'Result) = Length (Left)
|
|
|
1025 - M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
1026 + Length (Right)
|
|
|
1027
|
|
|
1028 -- Elements of Left and Right are in the result of Union
|
|
|
1029
|
|
|
1030 and Model (Left) <= Model (Union'Result)
|
|
|
1031 and Model (Right) <= Model (Union'Result)
|
|
|
1032
|
|
|
1033 -- Elements of the result of union come from either Left or Right
|
|
|
1034
|
|
|
1035 and
|
|
|
1036 M.Included_In_Union
|
|
|
1037 (Model (Union'Result), Model (Left), Model (Right))
|
|
|
1038
|
|
|
1039 -- Actual value of elements come from either Left or Right
|
|
|
1040
|
|
|
1041 and
|
|
|
1042 E_Elements_Included
|
|
|
1043 (Elements (Union'Result),
|
|
|
1044 Model (Left),
|
|
|
1045 Elements (Left),
|
|
|
1046 Elements (Right))
|
|
|
1047 and
|
|
|
1048 E_Elements_Included
|
|
|
1049 (Elements (Left), Model (Left), Elements (Union'Result))
|
|
|
1050 and
|
|
|
1051 E_Elements_Included
|
|
|
1052 (Elements (Right),
|
|
|
1053 Model (Left),
|
|
|
1054 Elements (Right),
|
|
|
1055 Elements (Union'Result));
|
|
|
1056
|
|
|
1057 function "or" (Left, Right : Set) return Set renames Union;
|
|
|
1058
|
|
|
1059 procedure Intersection (Target : in out Set; Source : Set) with
|
|
|
1060 Global => null,
|
|
|
1061 Post =>
|
|
|
1062 Length (Target) =
|
|
|
1063 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
1064
|
|
|
1065 -- Elements of Target were already in Target
|
|
|
1066
|
|
|
1067 and Model (Target) <= Model (Target)'Old
|
|
|
1068
|
|
|
1069 -- Elements of Target are in Source
|
|
|
1070
|
|
|
1071 and Model (Target) <= Model (Source)
|
|
|
1072
|
|
|
1073 -- Elements both in Source and Target are in the intersection
|
|
|
1074
|
|
|
1075 and
|
|
|
1076 M.Includes_Intersection
|
|
|
1077 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
1078
|
|
|
1079 -- Actual value of elements of Target is preserved
|
|
|
1080
|
|
|
1081 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
1082 and
|
|
|
1083 E_Elements_Included
|
|
|
1084 (Elements (Target)'Old, Model (Source), Elements (Target))
|
|
|
1085
|
|
|
1086 -- Mapping from cursors of Target to elements is preserved
|
|
|
1087
|
|
|
1088 and Mapping_Preserved
|
|
|
1089 (E_Left => Elements (Target),
|
|
|
1090 E_Right => Elements (Target)'Old,
|
|
|
1091 P_Left => Positions (Target),
|
|
|
1092 P_Right => Positions (Target)'Old);
|
|
|
1093
|
|
|
1094 function Intersection (Left, Right : Set) return Set with
|
|
|
1095 Global => null,
|
|
|
1096 Post =>
|
|
|
1097 Length (Intersection'Result) =
|
|
|
1098 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
1099
|
|
|
1100 -- Elements in the result of Intersection are in Left and Right
|
|
|
1101
|
|
|
1102 and Model (Intersection'Result) <= Model (Left)
|
|
|
1103 and Model (Intersection'Result) <= Model (Right)
|
|
|
1104
|
|
|
1105 -- Elements both in Left and Right are in the result of Intersection
|
|
|
1106
|
|
|
1107 and
|
|
|
1108 M.Includes_Intersection
|
|
|
1109 (Model (Intersection'Result), Model (Left), Model (Right))
|
|
|
1110
|
|
|
1111 -- Actual value of elements come from Left
|
|
|
1112
|
|
|
1113 and
|
|
|
1114 E_Elements_Included
|
|
|
1115 (Elements (Intersection'Result), Elements (Left))
|
|
|
1116 and
|
|
|
1117 E_Elements_Included
|
|
|
1118 (Elements (Left), Model (Right), Elements (Intersection'Result));
|
|
|
1119
|
|
|
1120 function "and" (Left, Right : Set) return Set renames Intersection;
|
|
|
1121
|
|
|
1122 procedure Difference (Target : in out Set; Source : Set) with
|
|
|
1123 Global => null,
|
|
|
1124 Post =>
|
|
|
1125 Length (Target) = Length (Target)'Old -
|
|
|
1126 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
1127
|
|
|
1128 -- Elements of Target were already in Target
|
|
|
1129
|
|
|
1130 and Model (Target) <= Model (Target)'Old
|
|
|
1131
|
|
|
1132 -- Elements of Target are not in Source
|
|
|
1133
|
|
|
1134 and M.No_Overlap (Model (Target), Model (Source))
|
|
|
1135
|
|
|
1136 -- Elements in Target but not in Source are in the difference
|
|
|
1137
|
|
|
1138 and
|
|
|
1139 M.Included_In_Union
|
|
|
1140 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
1141
|
|
|
1142 -- Actual value of elements of Target is preserved
|
|
|
1143
|
|
|
1144 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
1145 and
|
|
|
1146 E_Elements_Included
|
|
|
1147 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
1148
|
|
|
1149 -- Mapping from cursors of Target to elements is preserved
|
|
|
1150
|
|
|
1151 and Mapping_Preserved
|
|
|
1152 (E_Left => Elements (Target),
|
|
|
1153 E_Right => Elements (Target)'Old,
|
|
|
1154 P_Left => Positions (Target),
|
|
|
1155 P_Right => Positions (Target)'Old);
|
|
|
1156
|
|
|
1157 function Difference (Left, Right : Set) return Set with
|
|
|
1158 Global => null,
|
|
|
1159 Post =>
|
|
|
1160 Length (Difference'Result) = Length (Left) -
|
|
|
1161 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
1162
|
|
|
1163 -- Elements of the result of Difference are in Left
|
|
|
1164
|
|
|
1165 and Model (Difference'Result) <= Model (Left)
|
|
|
1166
|
|
|
1167 -- Elements of the result of Difference are in Right
|
|
|
1168
|
|
|
1169 and M.No_Overlap (Model (Difference'Result), Model (Right))
|
|
|
1170
|
|
|
1171 -- Elements in Left but not in Right are in the difference
|
|
|
1172
|
|
|
1173 and
|
|
|
1174 M.Included_In_Union
|
|
|
1175 (Model (Left), Model (Difference'Result), Model (Right))
|
|
|
1176
|
|
|
1177 -- Actual value of elements come from Left
|
|
|
1178
|
|
|
1179 and
|
|
|
1180 E_Elements_Included (Elements (Difference'Result), Elements (Left))
|
|
|
1181 and
|
|
|
1182 E_Elements_Included
|
|
|
1183 (Elements (Left),
|
|
|
1184 Model (Difference'Result),
|
|
|
1185 Elements (Difference'Result));
|
|
|
1186
|
|
|
1187 function "-" (Left, Right : Set) return Set renames Difference;
|
|
|
1188
|
|
|
1189 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
|
|
|
1190 Global => null,
|
|
|
1191 Pre =>
|
|
|
1192 Length (Source) - Length (Target and Source) <=
|
|
|
1193 Target.Capacity - Length (Target) + Length (Target and Source),
|
|
|
1194 Post =>
|
|
|
1195 Length (Target) = Length (Target)'Old -
|
|
|
1196 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
|
|
|
1197 Length (Source)
|
|
|
1198
|
|
|
1199 -- Elements of the difference were not both in Source and in Target
|
|
|
1200
|
|
|
1201 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
|
|
|
1202
|
|
|
1203 -- Elements in Target but not in Source are in the difference
|
|
|
1204
|
|
|
1205 and
|
|
|
1206 M.Included_In_Union
|
|
|
1207 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
1208
|
|
|
1209 -- Elements in Source but not in Target are in the difference
|
|
|
1210
|
|
|
1211 and
|
|
|
1212 M.Included_In_Union
|
|
|
1213 (Model (Source), Model (Target), Model (Target)'Old)
|
|
|
1214
|
|
|
1215 -- Actual value of elements come from either Left or Right
|
|
|
1216
|
|
|
1217 and
|
|
|
1218 E_Elements_Included
|
|
|
1219 (Elements (Target),
|
|
|
1220 Model (Target)'Old,
|
|
|
1221 Elements (Target)'Old,
|
|
|
1222 Elements (Source))
|
|
|
1223 and
|
|
|
1224 E_Elements_Included
|
|
|
1225 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
1226 and
|
|
|
1227 E_Elements_Included
|
|
|
1228 (Elements (Source), Model (Target), Elements (Target));
|
|
|
1229
|
|
|
1230 function Symmetric_Difference (Left, Right : Set) return Set with
|
|
|
1231 Global => null,
|
|
|
1232 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
1233 Post =>
|
|
|
1234 Length (Symmetric_Difference'Result) = Length (Left) -
|
|
|
1235 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
|
|
|
1236 Length (Right)
|
|
|
1237
|
|
|
1238 -- Elements of the difference were not both in Left and Right
|
|
|
1239
|
|
|
1240 and
|
|
|
1241 M.Not_In_Both
|
|
|
1242 (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
|
|
|
1243
|
|
|
1244 -- Elements in Left but not in Right are in the difference
|
|
|
1245
|
|
|
1246 and
|
|
|
1247 M.Included_In_Union
|
|
|
1248 (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
|
|
|
1249
|
|
|
1250 -- Elements in Right but not in Left are in the difference
|
|
|
1251
|
|
|
1252 and
|
|
|
1253 M.Included_In_Union
|
|
|
1254 (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
|
|
|
1255
|
|
|
1256 -- Actual value of elements come from either Left or Right
|
|
|
1257
|
|
|
1258 and
|
|
|
1259 E_Elements_Included
|
|
|
1260 (Elements (Symmetric_Difference'Result),
|
|
|
1261 Model (Left),
|
|
|
1262 Elements (Left),
|
|
|
1263 Elements (Right))
|
|
|
1264 and
|
|
|
1265 E_Elements_Included
|
|
|
1266 (Elements (Left),
|
|
|
1267 Model (Symmetric_Difference'Result),
|
|
|
1268 Elements (Symmetric_Difference'Result))
|
|
|
1269 and
|
|
|
1270 E_Elements_Included
|
|
|
1271 (Elements (Right),
|
|
|
1272 Model (Symmetric_Difference'Result),
|
|
|
1273 Elements (Symmetric_Difference'Result));
|
|
|
1274
|
|
|
1275 function "xor" (Left, Right : Set) return Set
|
|
|
1276 renames Symmetric_Difference;
|
|
|
1277
|
|
|
1278 function Overlap (Left, Right : Set) return Boolean with
|
|
|
1279 Global => null,
|
|
|
1280 Post =>
|
|
|
1281 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
|
|
|
1282
|
|
|
1283 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
|
|
|
1284 Global => null,
|
|
|
1285 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
|
|
|
1286
|
|
|
1287 function First (Container : Set) return Cursor with
|
|
|
1288 Global => null,
|
|
|
1289 Contract_Cases =>
|
|
|
1290 (Length (Container) = 0 =>
|
|
|
1291 First'Result = No_Element,
|
|
|
1292
|
|
|
1293 others =>
|
|
|
1294 Has_Element (Container, First'Result)
|
|
|
1295 and P.Get (Positions (Container), First'Result) = 1);
|
|
|
1296
|
|
|
1297 function First_Element (Container : Set) return Element_Type with
|
|
|
1298 Global => null,
|
|
|
1299 Pre => not Is_Empty (Container),
|
|
|
1300 Post =>
|
|
|
1301 First_Element'Result = E.Get (Elements (Container), 1)
|
|
|
1302 and E_Smaller_Than_Range
|
|
|
1303 (Elements (Container),
|
|
|
1304 2,
|
|
|
1305 Length (Container),
|
|
|
1306 First_Element'Result);
|
|
|
1307
|
|
|
1308 function Last (Container : Set) return Cursor with
|
|
|
1309 Global => null,
|
|
|
1310 Contract_Cases =>
|
|
|
1311 (Length (Container) = 0 =>
|
|
|
1312 Last'Result = No_Element,
|
|
|
1313
|
|
|
1314 others =>
|
|
|
1315 Has_Element (Container, Last'Result)
|
|
|
1316 and P.Get (Positions (Container), Last'Result) =
|
|
|
1317 Length (Container));
|
|
|
1318
|
|
|
1319 function Last_Element (Container : Set) return Element_Type with
|
|
|
1320 Global => null,
|
|
|
1321 Pre => not Is_Empty (Container),
|
|
|
1322 Post =>
|
|
|
1323 Last_Element'Result = E.Get (Elements (Container), Length (Container))
|
|
|
1324 and E_Bigger_Than_Range
|
|
|
1325 (Elements (Container),
|
|
|
1326 1,
|
|
|
1327 Length (Container) - 1,
|
|
|
1328 Last_Element'Result);
|
|
|
1329
|
|
|
1330 function Next (Container : Set; Position : Cursor) return Cursor with
|
|
|
1331 Global => null,
|
|
|
1332 Pre =>
|
|
|
1333 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1334 Contract_Cases =>
|
|
|
1335 (Position = No_Element
|
|
|
1336 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1337 =>
|
|
|
1338 Next'Result = No_Element,
|
|
|
1339
|
|
|
1340 others =>
|
|
|
1341 Has_Element (Container, Next'Result)
|
|
|
1342 and then P.Get (Positions (Container), Next'Result) =
|
|
|
1343 P.Get (Positions (Container), Position) + 1);
|
|
|
1344
|
|
|
1345 procedure Next (Container : Set; Position : in out Cursor) with
|
|
|
1346 Global => null,
|
|
|
1347 Pre =>
|
|
|
1348 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1349 Contract_Cases =>
|
|
|
1350 (Position = No_Element
|
|
|
1351 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1352 =>
|
|
|
1353 Position = No_Element,
|
|
|
1354
|
|
|
1355 others =>
|
|
|
1356 Has_Element (Container, Position)
|
|
|
1357 and then P.Get (Positions (Container), Position) =
|
|
|
1358 P.Get (Positions (Container), Position'Old) + 1);
|
|
|
1359
|
|
|
1360 function Previous (Container : Set; Position : Cursor) return Cursor with
|
|
|
1361 Global => null,
|
|
|
1362 Pre =>
|
|
|
1363 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1364 Contract_Cases =>
|
|
|
1365 (Position = No_Element
|
|
|
1366 or else P.Get (Positions (Container), Position) = 1
|
|
|
1367 =>
|
|
|
1368 Previous'Result = No_Element,
|
|
|
1369
|
|
|
1370 others =>
|
|
|
1371 Has_Element (Container, Previous'Result)
|
|
|
1372 and then P.Get (Positions (Container), Previous'Result) =
|
|
|
1373 P.Get (Positions (Container), Position) - 1);
|
|
|
1374
|
|
|
1375 procedure Previous (Container : Set; Position : in out Cursor) with
|
|
|
1376 Global => null,
|
|
|
1377 Pre =>
|
|
|
1378 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1379 Contract_Cases =>
|
|
|
1380 (Position = No_Element
|
|
|
1381 or else P.Get (Positions (Container), Position) = 1
|
|
|
1382 =>
|
|
|
1383 Position = No_Element,
|
|
|
1384
|
|
|
1385 others =>
|
|
|
1386 Has_Element (Container, Position)
|
|
|
1387 and then P.Get (Positions (Container), Position) =
|
|
|
1388 P.Get (Positions (Container), Position'Old) - 1);
|
|
|
1389
|
|
|
1390 function Find (Container : Set; Item : Element_Type) return Cursor with
|
|
|
1391 Global => null,
|
|
|
1392 Contract_Cases =>
|
|
|
1393
|
|
|
1394 -- If Item is not contained in Container, Find returns No_Element
|
|
|
1395
|
|
|
1396 (not Contains (Model (Container), Item) =>
|
|
|
1397 not P.Has_Key (Positions (Container), Find'Result)
|
|
|
1398 and Find'Result = No_Element,
|
|
|
1399
|
|
|
1400 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1401
|
|
|
1402 others =>
|
|
|
1403 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1404 and P.Get (Positions (Container), Find'Result) =
|
|
|
1405 Find (Elements (Container), Item)
|
|
|
1406
|
|
|
1407 -- The element designated by the result of Find is Item
|
|
|
1408
|
|
|
1409 and Equivalent_Elements
|
|
|
1410 (Element (Container, Find'Result), Item));
|
|
|
1411
|
|
|
1412 function Floor (Container : Set; Item : Element_Type) return Cursor with
|
|
|
1413 Global => null,
|
|
|
1414 Contract_Cases =>
|
|
|
1415 (Length (Container) = 0 or else Item < First_Element (Container) =>
|
|
|
1416 Floor'Result = No_Element,
|
|
|
1417 others =>
|
|
|
1418 Has_Element (Container, Floor'Result)
|
|
|
1419 and
|
|
|
1420 not (Item < E.Get (Elements (Container),
|
|
|
1421 P.Get (Positions (Container), Floor'Result)))
|
|
|
1422 and E_Is_Find
|
|
|
1423 (Elements (Container),
|
|
|
1424 Item,
|
|
|
1425 P.Get (Positions (Container), Floor'Result)));
|
|
|
1426
|
|
|
1427 function Ceiling (Container : Set; Item : Element_Type) return Cursor with
|
|
|
1428 Global => null,
|
|
|
1429 Contract_Cases =>
|
|
|
1430 (Length (Container) = 0 or else Last_Element (Container) < Item =>
|
|
|
1431 Ceiling'Result = No_Element,
|
|
|
1432 others =>
|
|
|
1433 Has_Element (Container, Ceiling'Result)
|
|
|
1434 and
|
|
|
1435 not (E.Get (Elements (Container),
|
|
|
1436 P.Get (Positions (Container), Ceiling'Result)) <
|
|
|
1437 Item)
|
|
|
1438 and E_Is_Find
|
|
|
1439 (Elements (Container),
|
|
|
1440 Item,
|
|
|
1441 P.Get (Positions (Container), Ceiling'Result)));
|
|
|
1442
|
|
|
1443 function Contains (Container : Set; Item : Element_Type) return Boolean with
|
|
|
1444 Global => null,
|
|
|
1445 Post => Contains'Result = Contains (Model (Container), Item);
|
|
|
1446 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
|
|
|
1447
|
|
|
1448 function Has_Element (Container : Set; Position : Cursor) return Boolean
|
|
|
1449 with
|
|
|
1450 Global => null,
|
|
|
1451 Post =>
|
|
|
1452 Has_Element'Result = P.Has_Key (Positions (Container), Position);
|
|
|
1453 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
|
|
|
1454
|
|
|
1455 generic
|
|
|
1456 type Key_Type (<>) is private;
|
|
|
1457
|
|
|
1458 with function Key (Element : Element_Type) return Key_Type;
|
|
|
1459
|
|
|
1460 with function "<" (Left, Right : Key_Type) return Boolean is <>;
|
|
|
1461
|
|
|
1462 package Generic_Keys with SPARK_Mode is
|
|
|
1463
|
|
|
1464 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
|
|
|
1465 Global => null,
|
|
|
1466 Post =>
|
|
|
1467 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left));
|
|
|
1468 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys);
|
|
|
1469
|
|
|
1470 package Formal_Model with Ghost is
|
|
|
1471 function E_Bigger_Than_Range
|
|
|
1472 (Container : E.Sequence;
|
|
|
1473 Fst : Positive_Count_Type;
|
|
|
1474 Lst : Count_Type;
|
|
|
1475 Key : Key_Type) return Boolean
|
|
|
1476 with
|
|
|
1477 Global => null,
|
|
|
1478 Pre => Lst <= E.Length (Container),
|
|
|
1479 Post =>
|
|
|
1480 E_Bigger_Than_Range'Result =
|
|
|
1481 (for all I in Fst .. Lst =>
|
|
|
1482 Generic_Keys.Key (E.Get (Container, I)) < Key);
|
|
|
1483 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
|
|
|
1484
|
|
|
1485 function E_Smaller_Than_Range
|
|
|
1486 (Container : E.Sequence;
|
|
|
1487 Fst : Positive_Count_Type;
|
|
|
1488 Lst : Count_Type;
|
|
|
1489 Key : Key_Type) return Boolean
|
|
|
1490 with
|
|
|
1491 Global => null,
|
|
|
1492 Pre => Lst <= E.Length (Container),
|
|
|
1493 Post =>
|
|
|
1494 E_Smaller_Than_Range'Result =
|
|
|
1495 (for all I in Fst .. Lst =>
|
|
|
1496 Key < Generic_Keys.Key (E.Get (Container, I)));
|
|
|
1497 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
|
|
|
1498
|
|
|
1499 function E_Is_Find
|
|
|
1500 (Container : E.Sequence;
|
|
|
1501 Key : Key_Type;
|
|
|
1502 Position : Count_Type) return Boolean
|
|
|
1503 with
|
|
|
1504 Global => null,
|
|
|
1505 Pre => Position - 1 <= E.Length (Container),
|
|
|
1506 Post =>
|
|
|
1507 E_Is_Find'Result =
|
|
|
1508
|
|
|
1509 ((if Position > 0 then
|
|
|
1510 E_Bigger_Than_Range (Container, 1, Position - 1, Key))
|
|
|
1511
|
|
|
1512 and (if Position < E.Length (Container) then
|
|
|
1513 E_Smaller_Than_Range
|
|
|
1514 (Container,
|
|
|
1515 Position + 1,
|
|
|
1516 E.Length (Container),
|
|
|
1517 Key)));
|
|
|
1518 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
|
|
|
1519
|
|
|
1520 function Find
|
|
|
1521 (Container : E.Sequence;
|
|
|
1522 Key : Key_Type) return Count_Type
|
|
|
1523 -- Search for Key in Container
|
|
|
1524
|
|
|
1525 with
|
|
|
1526 Global => null,
|
|
|
1527 Post =>
|
|
|
1528 (if Find'Result > 0 then
|
|
|
1529 Find'Result <= E.Length (Container)
|
|
|
1530 and Equivalent_Keys
|
|
|
1531 (Key, Generic_Keys.Key (E.Get (Container, Find'Result)))
|
|
|
1532 and E_Is_Find (Container, Key, Find'Result));
|
|
|
1533
|
|
|
1534 function M_Included_Except
|
|
|
1535 (Left : M.Set;
|
|
|
1536 Right : M.Set;
|
|
|
1537 Key : Key_Type) return Boolean
|
|
|
1538 with
|
|
|
1539 Global => null,
|
|
|
1540 Post =>
|
|
|
1541 M_Included_Except'Result =
|
|
|
1542 (for all E of Left =>
|
|
|
1543 Contains (Right, E)
|
|
|
1544 or Equivalent_Keys (Generic_Keys.Key (E), Key));
|
|
|
1545 end Formal_Model;
|
|
|
1546 use Formal_Model;
|
|
|
1547
|
|
|
1548 function Key (Container : Set; Position : Cursor) return Key_Type with
|
|
|
1549 Global => null,
|
|
|
1550 Post => Key'Result = Key (Element (Container, Position));
|
|
|
1551 pragma Annotate (GNATprove, Inline_For_Proof, Key);
|
|
|
1552
|
|
|
1553 function Element (Container : Set; Key : Key_Type) return Element_Type
|
|
|
1554 with
|
|
|
1555 Global => null,
|
|
|
1556 Pre => Contains (Container, Key),
|
|
|
1557 Post =>
|
|
|
1558 Element'Result = Element (Container, Find (Container, Key));
|
|
|
1559 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
1560
|
|
|
1561 procedure Replace
|
|
|
1562 (Container : in out Set;
|
|
|
1563 Key : Key_Type;
|
|
|
1564 New_Item : Element_Type)
|
|
|
1565 with
|
|
|
1566 Global => null,
|
|
|
1567 Pre => Contains (Container, Key),
|
|
|
1568 Post =>
|
|
|
1569 Length (Container) = Length (Container)'Old
|
|
|
1570
|
|
|
1571 -- Key now maps to New_Item
|
|
|
1572
|
|
|
1573 and Element (Container, Key) = New_Item
|
|
|
1574
|
|
|
1575 -- New_Item is contained in Container
|
|
|
1576
|
|
|
1577 and Contains (Model (Container), New_Item)
|
|
|
1578
|
|
|
1579 -- Other elements are preserved
|
|
|
1580
|
|
|
1581 and M_Included_Except
|
|
|
1582 (Model (Container)'Old,
|
|
|
1583 Model (Container),
|
|
|
1584 Key)
|
|
|
1585 and M.Included_Except
|
|
|
1586 (Model (Container),
|
|
|
1587 Model (Container)'Old,
|
|
|
1588 New_Item)
|
|
|
1589
|
|
|
1590 -- Mapping from cursors to elements is preserved
|
|
|
1591
|
|
|
1592 and Mapping_Preserved_Except
|
|
|
1593 (E_Left => Elements (Container)'Old,
|
|
|
1594 E_Right => Elements (Container),
|
|
|
1595 P_Left => Positions (Container)'Old,
|
|
|
1596 P_Right => Positions (Container),
|
|
|
1597 Position => Find (Container, Key))
|
|
|
1598 and Positions (Container) = Positions (Container)'Old;
|
|
|
1599
|
|
|
1600 procedure Exclude (Container : in out Set; Key : Key_Type) with
|
|
|
1601 Global => null,
|
|
|
1602 Post => not Contains (Container, Key),
|
|
|
1603 Contract_Cases =>
|
|
|
1604
|
|
|
1605 -- If Key is not in Container, nothing is changed
|
|
|
1606
|
|
|
1607 (not Contains (Container, Key) =>
|
|
|
1608 Model (Container) = Model (Container)'Old
|
|
|
1609 and Elements (Container) = Elements (Container)'Old
|
|
|
1610 and Positions (Container) = Positions (Container)'Old,
|
|
|
1611
|
|
|
1612 -- Otherwise, Key is removed from Container
|
|
|
1613
|
|
|
1614 others =>
|
|
|
1615 Length (Container) = Length (Container)'Old - 1
|
|
|
1616
|
|
|
1617 -- Other elements are preserved
|
|
|
1618
|
|
|
1619 and Model (Container) <= Model (Container)'Old
|
|
|
1620 and M_Included_Except
|
|
|
1621 (Model (Container)'Old,
|
|
|
1622 Model (Container),
|
|
|
1623 Key)
|
|
|
1624
|
|
|
1625 -- The elements of Container located before Key are preserved
|
|
|
1626
|
|
|
1627 and E.Range_Equal
|
|
|
1628 (Left => Elements (Container)'Old,
|
|
|
1629 Right => Elements (Container),
|
|
|
1630 Fst => 1,
|
|
|
1631 Lst => Find (Elements (Container), Key)'Old - 1)
|
|
|
1632
|
|
|
1633 -- The elements located after Key are shifted by 1
|
|
|
1634
|
|
|
1635 and E.Range_Shifted
|
|
|
1636 (Left => Elements (Container),
|
|
|
1637 Right => Elements (Container)'Old,
|
|
|
1638 Fst => Find (Elements (Container), Key)'Old,
|
|
|
1639 Lst => Length (Container),
|
|
|
1640 Offset => 1)
|
|
|
1641
|
|
|
1642 -- A cursor has been removed from Container
|
|
|
1643
|
|
|
1644 and P_Positions_Shifted
|
|
|
1645 (Positions (Container),
|
|
|
1646 Positions (Container)'Old,
|
|
|
1647 Cut => Find (Elements (Container), Key)'Old));
|
|
|
1648
|
|
|
1649 procedure Delete (Container : in out Set; Key : Key_Type) with
|
|
|
1650 Global => null,
|
|
|
1651 Pre => Contains (Container, Key),
|
|
|
1652 Post =>
|
|
|
1653 Length (Container) = Length (Container)'Old - 1
|
|
|
1654
|
|
|
1655 -- Key is no longer in Container
|
|
|
1656
|
|
|
1657 and not Contains (Container, Key)
|
|
|
1658
|
|
|
1659 -- Other elements are preserved
|
|
|
1660
|
|
|
1661 and Model (Container) <= Model (Container)'Old
|
|
|
1662 and M_Included_Except
|
|
|
1663 (Model (Container)'Old,
|
|
|
1664 Model (Container),
|
|
|
1665 Key)
|
|
|
1666
|
|
|
1667 -- The elements of Container located before Key are preserved
|
|
|
1668
|
|
|
1669 and E.Range_Equal
|
|
|
1670 (Left => Elements (Container)'Old,
|
|
|
1671 Right => Elements (Container),
|
|
|
1672 Fst => 1,
|
|
|
1673 Lst => Find (Elements (Container), Key)'Old - 1)
|
|
|
1674
|
|
|
1675 -- The elements located after Key are shifted by 1
|
|
|
1676
|
|
|
1677 and E.Range_Shifted
|
|
|
1678 (Left => Elements (Container),
|
|
|
1679 Right => Elements (Container)'Old,
|
|
|
1680 Fst => Find (Elements (Container), Key)'Old,
|
|
|
1681 Lst => Length (Container),
|
|
|
1682 Offset => 1)
|
|
|
1683
|
|
|
1684 -- A cursor has been removed from Container
|
|
|
1685
|
|
|
1686 and P_Positions_Shifted
|
|
|
1687 (Positions (Container),
|
|
|
1688 Positions (Container)'Old,
|
|
|
1689 Cut => Find (Elements (Container), Key)'Old);
|
|
|
1690
|
|
|
1691 function Find (Container : Set; Key : Key_Type) return Cursor with
|
|
|
1692 Global => null,
|
|
|
1693 Contract_Cases =>
|
|
|
1694
|
|
|
1695 -- If Key is not contained in Container, Find returns No_Element
|
|
|
1696
|
|
|
1697 ((for all E of Model (Container) =>
|
|
|
1698 not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
|
|
|
1699 not P.Has_Key (Positions (Container), Find'Result)
|
|
|
1700 and Find'Result = No_Element,
|
|
|
1701
|
|
|
1702 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1703
|
|
|
1704 others =>
|
|
|
1705 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1706 and P.Get (Positions (Container), Find'Result) =
|
|
|
1707 Find (Elements (Container), Key)
|
|
|
1708
|
|
|
1709 -- The element designated by the result of Find is Key
|
|
|
1710
|
|
|
1711 and Equivalent_Keys
|
|
|
1712 (Generic_Keys.Key (Element (Container, Find'Result)), Key));
|
|
|
1713
|
|
|
1714 function Floor (Container : Set; Key : Key_Type) return Cursor with
|
|
|
1715 Global => null,
|
|
|
1716 Contract_Cases =>
|
|
|
1717 (Length (Container) = 0
|
|
|
1718 or else Key < Generic_Keys.Key (First_Element (Container)) =>
|
|
|
1719 Floor'Result = No_Element,
|
|
|
1720 others =>
|
|
|
1721 Has_Element (Container, Floor'Result)
|
|
|
1722 and
|
|
|
1723 not (Key <
|
|
|
1724 Generic_Keys.Key
|
|
|
1725 (E.Get (Elements (Container),
|
|
|
1726 P.Get (Positions (Container), Floor'Result))))
|
|
|
1727 and E_Is_Find
|
|
|
1728 (Elements (Container),
|
|
|
1729 Key,
|
|
|
1730 P.Get (Positions (Container), Floor'Result)));
|
|
|
1731
|
|
|
1732 function Ceiling (Container : Set; Key : Key_Type) return Cursor with
|
|
|
1733 Global => null,
|
|
|
1734 Contract_Cases =>
|
|
|
1735 (Length (Container) = 0
|
|
|
1736 or else Generic_Keys.Key (Last_Element (Container)) < Key =>
|
|
|
1737 Ceiling'Result = No_Element,
|
|
|
1738 others =>
|
|
|
1739 Has_Element (Container, Ceiling'Result)
|
|
|
1740 and
|
|
|
1741 not (Generic_Keys.Key
|
|
|
1742 (E.Get (Elements (Container),
|
|
|
1743 P.Get (Positions (Container), Ceiling'Result)))
|
|
|
1744 < Key)
|
|
|
1745 and E_Is_Find
|
|
|
1746 (Elements (Container),
|
|
|
1747 Key,
|
|
|
1748 P.Get (Positions (Container), Ceiling'Result)));
|
|
|
1749
|
|
|
1750 function Contains (Container : Set; Key : Key_Type) return Boolean with
|
|
|
1751 Global => null,
|
|
|
1752 Post =>
|
|
|
1753 Contains'Result =
|
|
|
1754 (for some E of Model (Container) =>
|
|
|
1755 Equivalent_Keys (Key, Generic_Keys.Key (E)));
|
|
|
1756
|
|
|
1757 end Generic_Keys;
|
|
|
1758
|
|
|
1759 private
|
|
|
1760 pragma SPARK_Mode (Off);
|
|
|
1761
|
|
|
1762 pragma Inline (Next);
|
|
|
1763 pragma Inline (Previous);
|
|
|
1764
|
|
|
1765 type Node_Type is record
|
|
|
1766 Has_Element : Boolean := False;
|
|
|
1767 Parent : Count_Type := 0;
|
|
|
1768 Left : Count_Type := 0;
|
|
|
1769 Right : Count_Type := 0;
|
|
|
1770 Color : Red_Black_Trees.Color_Type;
|
|
|
1771 Element : Element_Type;
|
|
|
1772 end record;
|
|
|
1773
|
|
|
1774 package Tree_Types is
|
|
|
1775 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
|
|
|
1776
|
|
|
1777 type Set (Capacity : Count_Type) is
|
|
|
1778 new Tree_Types.Tree_Type (Capacity) with null record;
|
|
|
1779
|
|
|
1780 use Red_Black_Trees;
|
|
|
1781
|
|
|
1782 Empty_Set : constant Set := (Capacity => 0, others => <>);
|
|
|
1783
|
|
|
1784 end Ada.Containers.Formal_Ordered_Sets;
|
