|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2014-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 -- Similar to Ada.Containers.Formal_Vectors. The main difference is that
|
|
|
33 -- Element_Type may be indefinite (but not an unconstrained array).
|
|
|
34
|
|
|
35 with Ada.Containers.Bounded_Holders;
|
|
|
36 with Ada.Containers.Functional_Vectors;
|
|
|
37
|
|
|
38 generic
|
|
|
39 type Index_Type is range <>;
|
|
|
40 type Element_Type (<>) is private;
|
|
145
|
41 with function "=" (Left, Right : Element_Type) return Boolean is <>;
|
|
131
|
42 Max_Size_In_Storage_Elements : Natural;
|
|
111
|
43 -- Maximum size of Vector elements in bytes. This has the same meaning as
|
|
|
44 -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
|
|
|
45 -- setting this too small can lead to erroneous execution; see comments in
|
|
|
46 -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
|
|
|
47 -- responsibility of clients to calculate the maximum size of all types in
|
|
|
48 -- the class.
|
|
|
49
|
|
|
50 Bounded : Boolean := True;
|
|
|
51 -- If True, the containers are bounded; the initial capacity is the maximum
|
|
|
52 -- size, and heap allocation will be avoided. If False, the containers can
|
|
|
53 -- grow via heap allocation.
|
|
|
54
|
|
|
55 package Ada.Containers.Formal_Indefinite_Vectors with
|
|
|
56 SPARK_Mode => On
|
|
|
57 is
|
|
|
58 pragma Annotate (CodePeer, Skip_Analysis);
|
|
|
59
|
|
|
60 subtype Extended_Index is Index_Type'Base
|
|
|
61 range Index_Type'First - 1 ..
|
|
|
62 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
|
|
|
63
|
|
|
64 No_Index : constant Extended_Index := Extended_Index'First;
|
|
|
65
|
|
|
66 Last_Count : constant Count_Type :=
|
|
|
67 (if Index_Type'Last < Index_Type'First then
|
|
|
68 0
|
|
|
69 elsif Index_Type'Last < -1
|
|
|
70 or else Index_Type'Pos (Index_Type'First) >
|
|
|
71 Index_Type'Pos (Index_Type'Last) - Count_Type'Last
|
|
|
72 then
|
|
|
73 Index_Type'Pos (Index_Type'Last) -
|
|
|
74 Index_Type'Pos (Index_Type'First) + 1
|
|
|
75 else
|
|
|
76 Count_Type'Last);
|
|
|
77 -- Maximal capacity of any vector. It is the minimum of the size of the
|
|
|
78 -- index range and the last possible Count_Type.
|
|
|
79
|
|
|
80 subtype Capacity_Range is Count_Type range 0 .. Last_Count;
|
|
|
81
|
|
|
82 type Vector (Capacity : Capacity_Range) is limited private with
|
|
|
83 Default_Initial_Condition => Is_Empty (Vector);
|
|
|
84 -- In the bounded case, Capacity is the capacity of the container, which
|
|
|
85 -- never changes. In the unbounded case, Capacity is the initial capacity
|
|
|
86 -- of the container, and operations such as Reserve_Capacity and Append can
|
|
|
87 -- increase the capacity. The capacity never shrinks, except in the case of
|
|
|
88 -- Clear.
|
|
|
89 --
|
|
|
90 -- Note that all objects of type Vector are constrained, including in the
|
|
|
91 -- unbounded case; you can't assign from one object to another if the
|
|
|
92 -- Capacity is different.
|
|
|
93
|
|
|
94 function Length (Container : Vector) return Capacity_Range with
|
|
|
95 Global => null,
|
|
|
96 Post => Length'Result <= Capacity (Container);
|
|
|
97
|
|
|
98 pragma Unevaluated_Use_Of_Old (Allow);
|
|
|
99
|
|
|
100 package Formal_Model with Ghost is
|
|
|
101
|
|
|
102 package M is new Ada.Containers.Functional_Vectors
|
|
|
103 (Index_Type => Index_Type,
|
|
|
104 Element_Type => Element_Type);
|
|
|
105
|
|
|
106 function "="
|
|
|
107 (Left : M.Sequence;
|
|
|
108 Right : M.Sequence) return Boolean renames M."=";
|
|
|
109
|
|
|
110 function "<"
|
|
|
111 (Left : M.Sequence;
|
|
|
112 Right : M.Sequence) return Boolean renames M."<";
|
|
|
113
|
|
|
114 function "<="
|
|
|
115 (Left : M.Sequence;
|
|
|
116 Right : M.Sequence) return Boolean renames M."<=";
|
|
|
117
|
|
|
118 function M_Elements_In_Union
|
|
|
119 (Container : M.Sequence;
|
|
|
120 Left : M.Sequence;
|
|
|
121 Right : M.Sequence) return Boolean
|
|
|
122 -- The elements of Container are contained in either Left or Right
|
|
|
123 with
|
|
|
124 Global => null,
|
|
|
125 Post =>
|
|
|
126 M_Elements_In_Union'Result =
|
|
|
127 (for all I in Index_Type'First .. M.Last (Container) =>
|
|
|
128 (for some J in Index_Type'First .. M.Last (Left) =>
|
|
|
129 Element (Container, I) = Element (Left, J))
|
|
|
130 or (for some J in Index_Type'First .. M.Last (Right) =>
|
|
|
131 Element (Container, I) = Element (Right, J)));
|
|
|
132 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
|
|
|
133
|
|
|
134 function M_Elements_Included
|
|
|
135 (Left : M.Sequence;
|
|
|
136 L_Fst : Index_Type := Index_Type'First;
|
|
|
137 L_Lst : Extended_Index;
|
|
|
138 Right : M.Sequence;
|
|
|
139 R_Fst : Index_Type := Index_Type'First;
|
|
|
140 R_Lst : Extended_Index) return Boolean
|
|
|
141 -- The elements of the slice from L_Fst to L_Lst in Left are contained
|
|
|
142 -- in the slide from R_Fst to R_Lst in Right.
|
|
|
143 with
|
|
|
144 Global => null,
|
|
|
145 Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
|
|
|
146 Post =>
|
|
|
147 M_Elements_Included'Result =
|
|
|
148 (for all I in L_Fst .. L_Lst =>
|
|
|
149 (for some J in R_Fst .. R_Lst =>
|
|
|
150 Element (Left, I) = Element (Right, J)));
|
|
|
151 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
|
|
|
152
|
|
|
153 function M_Elements_Reversed
|
|
|
154 (Left : M.Sequence;
|
|
|
155 Right : M.Sequence) return Boolean
|
|
|
156 -- Right is Left in reverse order
|
|
|
157 with
|
|
|
158 Global => null,
|
|
|
159 Post =>
|
|
|
160 M_Elements_Reversed'Result =
|
|
|
161 (M.Length (Left) = M.Length (Right)
|
|
|
162 and (for all I in Index_Type'First .. M.Last (Left) =>
|
|
|
163 Element (Left, I) =
|
|
|
164 Element (Right, M.Last (Left) - I + 1))
|
|
|
165 and (for all I in Index_Type'First .. M.Last (Right) =>
|
|
|
166 Element (Right, I) =
|
|
|
167 Element (Left, M.Last (Left) - I + 1)));
|
|
|
168 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
|
|
|
169
|
|
|
170 function M_Elements_Swapped
|
|
|
171 (Left : M.Sequence;
|
|
|
172 Right : M.Sequence;
|
|
|
173 X : Index_Type;
|
|
|
174 Y : Index_Type) return Boolean
|
|
|
175 -- Elements stored at X and Y are reversed in Left and Right
|
|
|
176 with
|
|
|
177 Global => null,
|
|
|
178 Pre => X <= M.Last (Left) and Y <= M.Last (Left),
|
|
|
179 Post =>
|
|
|
180 M_Elements_Swapped'Result =
|
|
|
181 (M.Length (Left) = M.Length (Right)
|
|
|
182 and Element (Left, X) = Element (Right, Y)
|
|
|
183 and Element (Left, Y) = Element (Right, X)
|
|
|
184 and M.Equal_Except (Left, Right, X, Y));
|
|
|
185 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
|
|
|
186
|
|
|
187 function Model (Container : Vector) return M.Sequence with
|
|
|
188 -- The high-level model of a vector is a sequence of elements. The
|
|
|
189 -- sequence really is similar to the vector itself. However, it is not
|
|
|
190 -- limited which allows usage of 'Old and 'Loop_Entry attributes.
|
|
|
191
|
|
|
192 Ghost,
|
|
|
193 Global => null,
|
|
|
194 Post => M.Length (Model'Result) = Length (Container);
|
|
|
195
|
|
|
196 function Element
|
|
|
197 (S : M.Sequence;
|
|
|
198 I : Index_Type) return Element_Type renames M.Get;
|
|
|
199 -- To improve readability of contracts, we rename the function used to
|
|
|
200 -- access an element in the model to Element.
|
|
|
201
|
|
|
202 end Formal_Model;
|
|
|
203 use Formal_Model;
|
|
|
204
|
|
|
205 function Empty_Vector return Vector with
|
|
|
206 Global => null,
|
|
|
207 Post => Length (Empty_Vector'Result) = 0;
|
|
|
208
|
|
|
209 function "=" (Left, Right : Vector) return Boolean with
|
|
|
210 Global => null,
|
|
|
211 Post => "="'Result = (Model (Left) = Model (Right));
|
|
|
212
|
|
|
213 function To_Vector
|
|
|
214 (New_Item : Element_Type;
|
|
|
215 Length : Capacity_Range) return Vector
|
|
|
216 with
|
|
|
217 Global => null,
|
|
|
218 Post =>
|
|
|
219 Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length
|
|
|
220 and M.Constant_Range
|
|
|
221 (Container => Model (To_Vector'Result),
|
|
|
222 Fst => Index_Type'First,
|
|
|
223 Lst => Last_Index (To_Vector'Result),
|
|
|
224 Item => New_Item);
|
|
|
225
|
|
|
226 function Capacity (Container : Vector) return Capacity_Range with
|
|
|
227 Global => null,
|
|
|
228 Post =>
|
|
|
229 Capacity'Result =
|
|
|
230 (if Bounded then
|
|
|
231 Container.Capacity
|
|
|
232 else
|
|
|
233 Capacity_Range'Last);
|
|
|
234 pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
|
|
|
235
|
|
|
236 procedure Reserve_Capacity
|
|
|
237 (Container : in out Vector;
|
|
|
238 Capacity : Capacity_Range)
|
|
|
239 with
|
|
|
240 Global => null,
|
|
|
241 Pre => (if Bounded then Capacity <= Container.Capacity),
|
|
|
242 Post => Model (Container) = Model (Container)'Old;
|
|
|
243
|
|
|
244 function Is_Empty (Container : Vector) return Boolean with
|
|
|
245 Global => null,
|
|
|
246 Post => Is_Empty'Result = (Length (Container) = 0);
|
|
|
247
|
|
|
248 procedure Clear (Container : in out Vector) with
|
|
|
249 Global => null,
|
|
|
250 Post => Length (Container) = 0;
|
|
|
251 -- Note that this reclaims storage in the unbounded case. You need to call
|
|
|
252 -- this before a container goes out of scope in order to avoid storage
|
|
|
253 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
|
|
|
254
|
|
|
255 procedure Assign (Target : in out Vector; Source : Vector) with
|
|
|
256 Global => null,
|
|
|
257 Pre => (if Bounded then Length (Source) <= Target.Capacity),
|
|
|
258 Post => Model (Target) = Model (Source);
|
|
|
259
|
|
|
260 function Copy
|
|
|
261 (Source : Vector;
|
|
|
262 Capacity : Capacity_Range := 0) return Vector
|
|
|
263 with
|
|
|
264 Global => null,
|
|
|
265 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
|
|
|
266 Post =>
|
|
|
267 Model (Copy'Result) = Model (Source)
|
|
|
268 and (if Capacity = 0 then
|
|
|
269 Copy'Result.Capacity = Length (Source)
|
|
|
270 else
|
|
|
271 Copy'Result.Capacity = Capacity);
|
|
|
272
|
|
|
273 procedure Move (Target : in out Vector; Source : in out Vector)
|
|
|
274 with
|
|
|
275 Global => null,
|
|
|
276 Pre => (if Bounded then Length (Source) <= Capacity (Target)),
|
|
|
277 Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
|
|
|
278
|
|
|
279 function Element
|
|
|
280 (Container : Vector;
|
|
|
281 Index : Index_Type) return Element_Type
|
|
|
282 with
|
|
|
283 Global => null,
|
|
|
284 Pre => Index in First_Index (Container) .. Last_Index (Container),
|
|
|
285 Post => Element'Result = Element (Model (Container), Index);
|
|
|
286 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
287
|
|
|
288 procedure Replace_Element
|
|
|
289 (Container : in out Vector;
|
|
|
290 Index : Index_Type;
|
|
|
291 New_Item : Element_Type)
|
|
|
292 with
|
|
|
293 Global => null,
|
|
|
294 Pre => Index in First_Index (Container) .. Last_Index (Container),
|
|
|
295 Post =>
|
|
|
296 Length (Container) = Length (Container)'Old
|
|
|
297
|
|
|
298 -- Container now has New_Item at index Index
|
|
|
299
|
|
|
300 and Element (Model (Container), Index) = New_Item
|
|
|
301
|
|
|
302 -- All other elements are preserved
|
|
|
303
|
|
|
304 and M.Equal_Except
|
|
|
305 (Left => Model (Container)'Old,
|
|
|
306 Right => Model (Container),
|
|
|
307 Position => Index);
|
|
|
308
|
|
|
309 procedure Insert
|
|
|
310 (Container : in out Vector;
|
|
|
311 Before : Extended_Index;
|
|
|
312 New_Item : Vector)
|
|
|
313 with
|
|
|
314 Global => null,
|
|
|
315 Pre =>
|
|
|
316 Length (Container) <= Capacity (Container) - Length (New_Item)
|
|
|
317 and (Before in Index_Type'First .. Last_Index (Container)
|
|
|
318 or (Before /= No_Index
|
|
|
319 and then Before - 1 = Last_Index (Container))),
|
|
|
320 Post =>
|
|
|
321 Length (Container) = Length (Container)'Old + Length (New_Item)
|
|
|
322
|
|
|
323 -- Elements located before Before in Container are preserved
|
|
|
324
|
|
|
325 and M.Range_Equal
|
|
|
326 (Left => Model (Container)'Old,
|
|
|
327 Right => Model (Container),
|
|
|
328 Fst => Index_Type'First,
|
|
|
329 Lst => Before - 1)
|
|
|
330
|
|
|
331 -- Elements of New_Item are inserted at position Before
|
|
|
332
|
|
|
333 and (if Length (New_Item) > 0 then
|
|
|
334 M.Range_Shifted
|
|
|
335 (Left => Model (New_Item),
|
|
|
336 Right => Model (Container),
|
|
|
337 Fst => Index_Type'First,
|
|
|
338 Lst => Last_Index (New_Item),
|
|
|
339 Offset => Count_Type (Before - Index_Type'First)))
|
|
|
340
|
|
|
341 -- Elements located after Before in Container are shifted
|
|
|
342
|
|
|
343 and M.Range_Shifted
|
|
|
344 (Left => Model (Container)'Old,
|
|
|
345 Right => Model (Container),
|
|
|
346 Fst => Before,
|
|
|
347 Lst => Last_Index (Container)'Old,
|
|
|
348 Offset => Length (New_Item));
|
|
|
349
|
|
|
350 procedure Insert
|
|
|
351 (Container : in out Vector;
|
|
|
352 Before : Extended_Index;
|
|
|
353 New_Item : Element_Type)
|
|
|
354 with
|
|
|
355 Global => null,
|
|
|
356 Pre =>
|
|
|
357 Length (Container) < Capacity (Container)
|
|
|
358 and then (Before in Index_Type'First .. Last_Index (Container) + 1),
|
|
|
359 Post =>
|
|
|
360 Length (Container) = Length (Container)'Old + 1
|
|
|
361
|
|
|
362 -- Elements located before Before in Container are preserved
|
|
|
363
|
|
|
364 and M.Range_Equal
|
|
|
365 (Left => Model (Container)'Old,
|
|
|
366 Right => Model (Container),
|
|
|
367 Fst => Index_Type'First,
|
|
|
368 Lst => Before - 1)
|
|
|
369
|
|
|
370 -- Container now has New_Item at index Before
|
|
|
371
|
|
|
372 and Element (Model (Container), Before) = New_Item
|
|
|
373
|
|
|
374 -- Elements located after Before in Container are shifted by 1
|
|
|
375
|
|
|
376 and M.Range_Shifted
|
|
|
377 (Left => Model (Container)'Old,
|
|
|
378 Right => Model (Container),
|
|
|
379 Fst => Before,
|
|
|
380 Lst => Last_Index (Container)'Old,
|
|
|
381 Offset => 1);
|
|
|
382
|
|
|
383 procedure Insert
|
|
|
384 (Container : in out Vector;
|
|
|
385 Before : Extended_Index;
|
|
|
386 New_Item : Element_Type;
|
|
|
387 Count : Count_Type)
|
|
|
388 with
|
|
|
389 Global => null,
|
|
|
390 Pre =>
|
|
|
391 Length (Container) <= Capacity (Container) - Count
|
|
|
392 and (Before in Index_Type'First .. Last_Index (Container)
|
|
|
393 or (Before /= No_Index
|
|
|
394 and then Before - 1 = Last_Index (Container))),
|
|
|
395 Post =>
|
|
|
396 Length (Container) = Length (Container)'Old + Count
|
|
|
397
|
|
|
398 -- Elements located before Before in Container are preserved
|
|
|
399
|
|
|
400 and M.Range_Equal
|
|
|
401 (Left => Model (Container)'Old,
|
|
|
402 Right => Model (Container),
|
|
|
403 Fst => Index_Type'First,
|
|
|
404 Lst => Before - 1)
|
|
|
405
|
|
|
406 -- New_Item is inserted Count times at position Before
|
|
|
407
|
|
|
408 and (if Count > 0 then
|
|
|
409 M.Constant_Range
|
|
|
410 (Container => Model (Container),
|
|
|
411 Fst => Before,
|
|
|
412 Lst => Before + Index_Type'Base (Count - 1),
|
|
|
413 Item => New_Item))
|
|
|
414
|
|
|
415 -- Elements located after Before in Container are shifted
|
|
|
416
|
|
|
417 and M.Range_Shifted
|
|
|
418 (Left => Model (Container)'Old,
|
|
|
419 Right => Model (Container),
|
|
|
420 Fst => Before,
|
|
|
421 Lst => Last_Index (Container)'Old,
|
|
|
422 Offset => Count);
|
|
|
423
|
|
|
424 procedure Prepend (Container : in out Vector; New_Item : Vector) with
|
|
|
425 Global => null,
|
|
|
426 Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
|
|
|
427 Post =>
|
|
|
428 Length (Container) = Length (Container)'Old + Length (New_Item)
|
|
|
429
|
|
|
430 -- Elements of New_Item are inserted at the beginning of Container
|
|
|
431
|
|
|
432 and M.Range_Equal
|
|
|
433 (Left => Model (New_Item),
|
|
|
434 Right => Model (Container),
|
|
|
435 Fst => Index_Type'First,
|
|
|
436 Lst => Last_Index (New_Item))
|
|
|
437
|
|
|
438 -- Elements of Container are shifted
|
|
|
439
|
|
|
440 and M.Range_Shifted
|
|
|
441 (Left => Model (Container)'Old,
|
|
|
442 Right => Model (Container),
|
|
|
443 Fst => Index_Type'First,
|
|
|
444 Lst => Last_Index (Container)'Old,
|
|
|
445 Offset => Length (New_Item));
|
|
|
446
|
|
|
447 procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
|
|
|
448 Global => null,
|
|
|
449 Pre => Length (Container) < Capacity (Container),
|
|
|
450 Post =>
|
|
|
451 Length (Container) = Length (Container)'Old + 1
|
|
|
452
|
|
|
453 -- Container now has New_Item at Index_Type'First
|
|
|
454
|
|
|
455 and Element (Model (Container), Index_Type'First) = New_Item
|
|
|
456
|
|
|
457 -- Elements of Container are shifted by 1
|
|
|
458
|
|
|
459 and M.Range_Shifted
|
|
|
460 (Left => Model (Container)'Old,
|
|
|
461 Right => Model (Container),
|
|
|
462 Fst => Index_Type'First,
|
|
|
463 Lst => Last_Index (Container)'Old,
|
|
|
464 Offset => 1);
|
|
|
465
|
|
|
466 procedure Prepend
|
|
|
467 (Container : in out Vector;
|
|
|
468 New_Item : Element_Type;
|
|
|
469 Count : Count_Type)
|
|
|
470 with
|
|
|
471 Global => null,
|
|
|
472 Pre => Length (Container) <= Capacity (Container) - Count,
|
|
|
473 Post =>
|
|
|
474 Length (Container) = Length (Container)'Old + Count
|
|
|
475
|
|
|
476 -- New_Item is inserted Count times at the beginning of Container
|
|
|
477
|
|
|
478 and M.Constant_Range
|
|
|
479 (Container => Model (Container),
|
|
|
480 Fst => Index_Type'First,
|
|
|
481 Lst => Index_Type'First + Index_Type'Base (Count - 1),
|
|
|
482 Item => New_Item)
|
|
|
483
|
|
|
484 -- Elements of Container are shifted
|
|
|
485
|
|
|
486 and M.Range_Shifted
|
|
|
487 (Left => Model (Container)'Old,
|
|
|
488 Right => Model (Container),
|
|
|
489 Fst => Index_Type'First,
|
|
|
490 Lst => Last_Index (Container)'Old,
|
|
|
491 Offset => Count);
|
|
|
492
|
|
|
493 procedure Append (Container : in out Vector; New_Item : Vector) with
|
|
|
494 Global => null,
|
|
|
495 Pre =>
|
|
|
496 Length (Container) <= Capacity (Container) - Length (New_Item),
|
|
|
497 Post =>
|
|
|
498 Length (Container) = Length (Container)'Old + Length (New_Item)
|
|
|
499
|
|
|
500 -- The elements of Container are preserved
|
|
|
501
|
|
|
502 and Model (Container)'Old <= Model (Container)
|
|
|
503
|
|
|
504 -- Elements of New_Item are inserted at the end of Container
|
|
|
505
|
|
|
506 and (if Length (New_Item) > 0 then
|
|
|
507 M.Range_Shifted
|
|
|
508 (Left => Model (New_Item),
|
|
|
509 Right => Model (Container),
|
|
|
510 Fst => Index_Type'First,
|
|
|
511 Lst => Last_Index (New_Item),
|
|
|
512 Offset =>
|
|
|
513 Count_Type
|
|
|
514 (Last_Index (Container)'Old - Index_Type'First + 1)));
|
|
|
515
|
|
|
516 procedure Append (Container : in out Vector; New_Item : Element_Type) with
|
|
|
517 Global => null,
|
|
|
518 Pre => Length (Container) < Capacity (Container),
|
|
|
519 Post =>
|
|
|
520 Length (Container) = Length (Container)'Old + 1
|
|
|
521
|
|
|
522 -- Elements of Container are preserved
|
|
|
523
|
|
|
524 and Model (Container)'Old < Model (Container)
|
|
|
525
|
|
|
526 -- Container now has New_Item at the end of Container
|
|
|
527
|
|
|
528 and Element
|
|
|
529 (Model (Container), Last_Index (Container)'Old + 1) = New_Item;
|
|
|
530
|
|
|
531 procedure Append
|
|
|
532 (Container : in out Vector;
|
|
|
533 New_Item : Element_Type;
|
|
|
534 Count : Count_Type)
|
|
|
535 with
|
|
|
536 Global => null,
|
|
|
537 Pre => Length (Container) <= Capacity (Container) - Count,
|
|
|
538 Post =>
|
|
|
539 Length (Container) = Length (Container)'Old + Count
|
|
|
540
|
|
|
541 -- Elements of Container are preserved
|
|
|
542
|
|
|
543 and Model (Container)'Old <= Model (Container)
|
|
|
544
|
|
|
545 -- New_Item is inserted Count times at the end of Container
|
|
|
546
|
|
|
547 and (if Count > 0 then
|
|
|
548 M.Constant_Range
|
|
|
549 (Container => Model (Container),
|
|
|
550 Fst => Last_Index (Container)'Old + 1,
|
|
|
551 Lst =>
|
|
|
552 Last_Index (Container)'Old + Index_Type'Base (Count),
|
|
|
553 Item => New_Item));
|
|
|
554
|
|
|
555 procedure Delete (Container : in out Vector; Index : Extended_Index) with
|
|
|
556 Global => null,
|
|
|
557 Pre => Index in First_Index (Container) .. Last_Index (Container),
|
|
|
558 Post =>
|
|
|
559 Length (Container) = Length (Container)'Old - 1
|
|
|
560
|
|
|
561 -- Elements located before Index in Container are preserved
|
|
|
562
|
|
|
563 and M.Range_Equal
|
|
|
564 (Left => Model (Container)'Old,
|
|
|
565 Right => Model (Container),
|
|
|
566 Fst => Index_Type'First,
|
|
|
567 Lst => Index - 1)
|
|
|
568
|
|
|
569 -- Elements located after Index in Container are shifted by 1
|
|
|
570
|
|
|
571 and M.Range_Shifted
|
|
|
572 (Left => Model (Container),
|
|
|
573 Right => Model (Container)'Old,
|
|
|
574 Fst => Index,
|
|
|
575 Lst => Last_Index (Container),
|
|
|
576 Offset => 1);
|
|
|
577
|
|
|
578 procedure Delete
|
|
|
579 (Container : in out Vector;
|
|
|
580 Index : Extended_Index;
|
|
|
581 Count : Count_Type)
|
|
|
582 with
|
|
|
583 Global => null,
|
|
|
584 Pre =>
|
|
|
585 Index in First_Index (Container) .. Last_Index (Container),
|
|
|
586 Post =>
|
|
|
587 Length (Container) in
|
|
|
588 Length (Container)'Old - Count .. Length (Container)'Old
|
|
|
589
|
|
|
590 -- The elements of Container located before Index are preserved.
|
|
|
591
|
|
|
592 and M.Range_Equal
|
|
|
593 (Left => Model (Container)'Old,
|
|
|
594 Right => Model (Container),
|
|
|
595 Fst => Index_Type'First,
|
|
|
596 Lst => Index - 1),
|
|
|
597
|
|
|
598 Contract_Cases =>
|
|
|
599
|
|
|
600 -- All the elements after Position have been erased
|
|
|
601
|
|
|
602 (Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
|
|
|
603 Length (Container) = Count_Type (Index - Index_Type'First),
|
|
|
604
|
|
|
605 others =>
|
|
|
606 Length (Container) = Length (Container)'Old - Count
|
|
|
607
|
|
|
608 -- Other elements are shifted by Count
|
|
|
609
|
|
|
610 and M.Range_Shifted
|
|
|
611 (Left => Model (Container),
|
|
|
612 Right => Model (Container)'Old,
|
|
|
613 Fst => Index,
|
|
|
614 Lst => Last_Index (Container),
|
|
|
615 Offset => Count));
|
|
|
616
|
|
|
617 procedure Delete_First (Container : in out Vector) with
|
|
|
618 Global => null,
|
|
|
619 Pre => Length (Container) > 0,
|
|
|
620 Post =>
|
|
|
621 Length (Container) = Length (Container)'Old - 1
|
|
|
622
|
|
|
623 -- Elements of Container are shifted by 1
|
|
|
624
|
|
|
625 and M.Range_Shifted
|
|
|
626 (Left => Model (Container),
|
|
|
627 Right => Model (Container)'Old,
|
|
|
628 Fst => Index_Type'First,
|
|
|
629 Lst => Last_Index (Container),
|
|
|
630 Offset => 1);
|
|
|
631
|
|
|
632 procedure Delete_First (Container : in out Vector; Count : Count_Type) with
|
|
|
633 Global => null,
|
|
|
634 Contract_Cases =>
|
|
|
635
|
|
|
636 -- All the elements of Container have been erased
|
|
|
637
|
|
|
638 (Length (Container) <= Count => Length (Container) = 0,
|
|
|
639
|
|
|
640 others =>
|
|
|
641 Length (Container) = Length (Container)'Old - Count
|
|
|
642
|
|
|
643 -- Elements of Container are shifted by Count
|
|
|
644
|
|
|
645 and M.Range_Shifted
|
|
|
646 (Left => Model (Container),
|
|
|
647 Right => Model (Container)'Old,
|
|
|
648 Fst => Index_Type'First,
|
|
|
649 Lst => Last_Index (Container),
|
|
|
650 Offset => Count));
|
|
|
651
|
|
|
652 procedure Delete_Last (Container : in out Vector) with
|
|
|
653 Global => null,
|
|
|
654 Pre => Length (Container) > 0,
|
|
|
655 Post =>
|
|
|
656 Length (Container) = Length (Container)'Old - 1
|
|
|
657
|
|
|
658 -- Elements of Container are preserved
|
|
|
659
|
|
|
660 and Model (Container) < Model (Container)'Old;
|
|
|
661
|
|
|
662 procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
|
|
|
663 Global => null,
|
|
|
664 Contract_Cases =>
|
|
|
665
|
|
|
666 -- All the elements after Position have been erased
|
|
|
667
|
|
|
668 (Length (Container) <= Count => Length (Container) = 0,
|
|
|
669
|
|
|
670 others =>
|
|
|
671 Length (Container) = Length (Container)'Old - Count
|
|
|
672
|
|
|
673 -- The elements of Container are preserved
|
|
|
674
|
|
|
675 and Model (Container) <= Model (Container)'Old);
|
|
|
676
|
|
|
677 procedure Reverse_Elements (Container : in out Vector) with
|
|
|
678 Global => null,
|
|
|
679 Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
|
|
|
680
|
|
|
681 procedure Swap
|
|
|
682 (Container : in out Vector;
|
|
|
683 I : Index_Type;
|
|
|
684 J : Index_Type)
|
|
|
685 with
|
|
|
686 Global => null,
|
|
|
687 Pre =>
|
|
|
688 I in First_Index (Container) .. Last_Index (Container)
|
|
|
689 and then J in First_Index (Container) .. Last_Index (Container),
|
|
|
690 Post =>
|
|
|
691 M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
|
|
|
692
|
|
|
693 function First_Index (Container : Vector) return Index_Type with
|
|
|
694 Global => null,
|
|
|
695 Post => First_Index'Result = Index_Type'First;
|
|
|
696 pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
|
|
|
697
|
|
|
698 function First_Element (Container : Vector) return Element_Type with
|
|
|
699 Global => null,
|
|
|
700 Pre => not Is_Empty (Container),
|
|
|
701 Post =>
|
|
|
702 First_Element'Result = Element (Model (Container), Index_Type'First);
|
|
|
703 pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
|
|
|
704
|
|
|
705 function Last_Index (Container : Vector) return Extended_Index with
|
|
|
706 Global => null,
|
|
|
707 Post => Last_Index'Result = M.Last (Model (Container));
|
|
|
708 pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
|
|
|
709
|
|
|
710 function Last_Element (Container : Vector) return Element_Type with
|
|
|
711 Global => null,
|
|
|
712 Pre => not Is_Empty (Container),
|
|
|
713 Post =>
|
|
|
714 Last_Element'Result =
|
|
|
715 Element (Model (Container), Last_Index (Container));
|
|
|
716 pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
|
|
|
717
|
|
|
718 function Find_Index
|
|
|
719 (Container : Vector;
|
|
|
720 Item : Element_Type;
|
|
|
721 Index : Index_Type := Index_Type'First) return Extended_Index
|
|
|
722 with
|
|
|
723 Global => null,
|
|
|
724 Contract_Cases =>
|
|
|
725
|
|
|
726 -- If Item is not contained in Container after Index, Find_Index
|
|
|
727 -- returns No_Index.
|
|
|
728
|
|
|
729 (Index > Last_Index (Container)
|
|
|
730 or else not M.Contains
|
|
|
731 (Container => Model (Container),
|
|
|
732 Fst => Index,
|
|
|
733 Lst => Last_Index (Container),
|
|
|
734 Item => Item)
|
|
|
735 =>
|
|
|
736 Find_Index'Result = No_Index,
|
|
|
737
|
|
|
738 -- Otherwise, Find_Index returns a valid index greater than Index
|
|
|
739
|
|
|
740 others =>
|
|
|
741 Find_Index'Result in Index .. Last_Index (Container)
|
|
|
742
|
|
|
743 -- The element at this index in Container is Item
|
|
|
744
|
|
|
745 and Element (Model (Container), Find_Index'Result) = Item
|
|
|
746
|
|
|
747 -- It is the first occurrence of Item after Index in Container
|
|
|
748
|
|
|
749 and not M.Contains
|
|
|
750 (Container => Model (Container),
|
|
|
751 Fst => Index,
|
|
|
752 Lst => Find_Index'Result - 1,
|
|
|
753 Item => Item));
|
|
|
754
|
|
|
755 function Reverse_Find_Index
|
|
|
756 (Container : Vector;
|
|
|
757 Item : Element_Type;
|
|
|
758 Index : Index_Type := Index_Type'Last) return Extended_Index
|
|
|
759 with
|
|
|
760 Global => null,
|
|
|
761 Contract_Cases =>
|
|
|
762
|
|
|
763 -- If Item is not contained in Container before Index,
|
|
|
764 -- Reverse_Find_Index returns No_Index.
|
|
|
765
|
|
|
766 (not M.Contains
|
|
|
767 (Container => Model (Container),
|
|
|
768 Fst => Index_Type'First,
|
|
|
769 Lst => (if Index <= Last_Index (Container) then Index
|
|
|
770 else Last_Index (Container)),
|
|
|
771 Item => Item)
|
|
|
772 =>
|
|
|
773 Reverse_Find_Index'Result = No_Index,
|
|
|
774
|
|
|
775 -- Otherwise, Reverse_Find_Index returns a valid index smaller than
|
|
|
776 -- Index
|
|
|
777
|
|
|
778 others =>
|
|
|
779 Reverse_Find_Index'Result in Index_Type'First .. Index
|
|
|
780 and Reverse_Find_Index'Result <= Last_Index (Container)
|
|
|
781
|
|
|
782 -- The element at this index in Container is Item
|
|
|
783
|
|
|
784 and Element (Model (Container), Reverse_Find_Index'Result) = Item
|
|
|
785
|
|
|
786 -- It is the last occurrence of Item before Index in Container
|
|
|
787
|
|
|
788 and not M.Contains
|
|
|
789 (Container => Model (Container),
|
|
|
790 Fst => Reverse_Find_Index'Result + 1,
|
|
|
791 Lst =>
|
|
|
792 (if Index <= Last_Index (Container) then
|
|
|
793 Index
|
|
|
794 else
|
|
|
795 Last_Index (Container)),
|
|
|
796 Item => Item));
|
|
|
797
|
|
|
798 function Contains
|
|
|
799 (Container : Vector;
|
|
|
800 Item : Element_Type) return Boolean
|
|
|
801 with
|
|
|
802 Global => null,
|
|
|
803 Post =>
|
|
|
804 Contains'Result =
|
|
|
805 M.Contains
|
|
|
806 (Container => Model (Container),
|
|
|
807 Fst => Index_Type'First,
|
|
|
808 Lst => Last_Index (Container),
|
|
|
809 Item => Item);
|
|
|
810
|
|
|
811 function Has_Element
|
|
|
812 (Container : Vector;
|
|
|
813 Position : Extended_Index) return Boolean
|
|
|
814 with
|
|
|
815 Global => null,
|
|
|
816 Post =>
|
|
|
817 Has_Element'Result =
|
|
|
818 (Position in Index_Type'First .. Last_Index (Container));
|
|
|
819 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
|
|
|
820
|
|
|
821 generic
|
|
|
822 with function "<" (Left, Right : Element_Type) return Boolean is <>;
|
|
|
823 package Generic_Sorting with SPARK_Mode is
|
|
|
824
|
|
|
825 package Formal_Model with Ghost is
|
|
|
826
|
|
|
827 function M_Elements_Sorted (Container : M.Sequence) return Boolean
|
|
|
828 with
|
|
|
829 Global => null,
|
|
|
830 Post =>
|
|
|
831 M_Elements_Sorted'Result =
|
|
|
832 (for all I in Index_Type'First .. M.Last (Container) =>
|
|
|
833 (for all J in I .. M.Last (Container) =>
|
|
|
834 Element (Container, I) = Element (Container, J)
|
|
|
835 or Element (Container, I) < Element (Container, J)));
|
|
|
836 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
|
|
|
837
|
|
|
838 end Formal_Model;
|
|
|
839 use Formal_Model;
|
|
|
840
|
|
|
841 function Is_Sorted (Container : Vector) return Boolean with
|
|
|
842 Global => null,
|
|
|
843 Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
|
|
|
844
|
|
|
845 procedure Sort (Container : in out Vector) with
|
|
|
846 Global => null,
|
|
|
847 Post =>
|
|
|
848 Length (Container) = Length (Container)'Old
|
|
|
849 and M_Elements_Sorted (Model (Container))
|
|
|
850 and M_Elements_Included
|
|
|
851 (Left => Model (Container)'Old,
|
|
|
852 L_Lst => Last_Index (Container),
|
|
|
853 Right => Model (Container),
|
|
|
854 R_Lst => Last_Index (Container))
|
|
|
855 and M_Elements_Included
|
|
|
856 (Left => Model (Container),
|
|
|
857 L_Lst => Last_Index (Container),
|
|
|
858 Right => Model (Container)'Old,
|
|
|
859 R_Lst => Last_Index (Container));
|
|
|
860
|
|
|
861 procedure Merge (Target : in out Vector; Source : in out Vector) with
|
|
|
862 -- Target and Source should not be aliased
|
|
|
863 Global => null,
|
|
|
864 Pre => Length (Source) <= Capacity (Target) - Length (Target),
|
|
|
865 Post =>
|
|
|
866 Length (Target) = Length (Target)'Old + Length (Source)'Old
|
|
|
867 and Length (Source) = 0
|
|
|
868 and (if M_Elements_Sorted (Model (Target)'Old)
|
|
|
869 and M_Elements_Sorted (Model (Source)'Old)
|
|
|
870 then
|
|
|
871 M_Elements_Sorted (Model (Target)))
|
|
|
872 and M_Elements_Included
|
|
|
873 (Left => Model (Target)'Old,
|
|
|
874 L_Lst => Last_Index (Target)'Old,
|
|
|
875 Right => Model (Target),
|
|
|
876 R_Lst => Last_Index (Target))
|
|
|
877 and M_Elements_Included
|
|
|
878 (Left => Model (Source)'Old,
|
|
|
879 L_Lst => Last_Index (Source)'Old,
|
|
|
880 Right => Model (Target),
|
|
|
881 R_Lst => Last_Index (Target))
|
|
|
882 and M_Elements_In_Union
|
|
|
883 (Model (Target),
|
|
|
884 Model (Source)'Old,
|
|
|
885 Model (Target)'Old);
|
|
|
886 end Generic_Sorting;
|
|
|
887
|
|
|
888 private
|
|
|
889 pragma SPARK_Mode (Off);
|
|
|
890
|
|
|
891 pragma Inline (First_Index);
|
|
|
892 pragma Inline (Last_Index);
|
|
|
893 pragma Inline (Element);
|
|
|
894 pragma Inline (First_Element);
|
|
|
895 pragma Inline (Last_Element);
|
|
|
896 pragma Inline (Replace_Element);
|
|
|
897 pragma Inline (Contains);
|
|
|
898
|
|
|
899 -- The implementation method is to instantiate Bounded_Holders to get a
|
|
|
900 -- definite type for Element_Type.
|
|
|
901
|
|
|
902 package Holders is new Bounded_Holders
|
|
|
903 (Element_Type, Max_Size_In_Storage_Elements, "=");
|
|
|
904 use Holders;
|
|
|
905
|
|
|
906 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
|
|
|
907 type Elements_Array is array (Array_Index range <>) of Holder;
|
|
|
908 function "=" (L, R : Elements_Array) return Boolean is abstract;
|
|
|
909
|
|
|
910 type Elements_Array_Ptr is access all Elements_Array;
|
|
|
911
|
|
|
912 type Vector (Capacity : Capacity_Range) is limited record
|
|
|
913
|
|
|
914 -- In the bounded case, the elements are stored in Elements. In the
|
|
|
915 -- unbounded case, the elements are initially stored in Elements, until
|
|
|
916 -- we run out of room, then we switch to Elements_Ptr.
|
|
|
917
|
|
|
918 Last : Extended_Index := No_Index;
|
|
|
919 Elements_Ptr : Elements_Array_Ptr := null;
|
|
|
920 Elements : aliased Elements_Array (1 .. Capacity);
|
|
|
921 end record;
|
|
|
922
|
|
|
923 -- The primary reason Vector is limited is that in the unbounded case, once
|
|
|
924 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
|
|
|
925 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
|
|
|
926 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would
|
|
|
927 -- allow SPARK to "prove" things that are false. We could fix that by
|
|
|
928 -- making Vector a controlled type, and override Adjust to make a deep
|
|
|
929 -- copy, but finalization is not allowed in SPARK.
|
|
|
930 --
|
|
|
931 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
|
|
|
932 -- allowed on Vectors.
|
|
|
933
|
|
|
934 function Empty_Vector return Vector is
|
|
|
935 ((Capacity => 0, others => <>));
|
|
|
936
|
|
|
937 end Ada.Containers.Formal_Indefinite_Vectors;
|
