|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- ADA.CONTAINERS.FUNCTIONAL_VECTORS --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2016-2019, Free Software Foundation, Inc. --
|
|
111
|
10 -- --
|
|
|
11 -- This specification is derived from the Ada Reference Manual for use with --
|
|
|
12 -- GNAT. The copyright notice above, and the license provisions that follow --
|
|
|
13 -- apply solely to the contents of the part following the private keyword. --
|
|
|
14 -- --
|
|
|
15 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
16 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
|
|
|
21 -- --
|
|
|
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
23 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
24 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
25 -- --
|
|
|
26 -- You should have received a copy of the GNU General Public License and --
|
|
|
27 -- a copy of the GCC Runtime Library Exception along with this program; --
|
|
|
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
|
|
29 -- <http://www.gnu.org/licenses/>. --
|
|
|
30 ------------------------------------------------------------------------------
|
|
|
31
|
|
|
32 pragma Ada_2012;
|
|
|
33 private with Ada.Containers.Functional_Base;
|
|
|
34
|
|
|
35 generic
|
|
|
36 type Index_Type is (<>);
|
|
|
37 -- To avoid Constraint_Error being raised at run time, Index_Type'Base
|
|
|
38 -- should have at least one more element at the low end than Index_Type.
|
|
|
39
|
|
|
40 type Element_Type (<>) is private;
|
|
145
|
41 with function "=" (Left, Right : Element_Type) return Boolean is <>;
|
|
111
|
42
|
|
|
43 package Ada.Containers.Functional_Vectors with SPARK_Mode is
|
|
|
44
|
|
|
45 subtype Extended_Index is Index_Type'Base range
|
|
|
46 Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
|
|
|
47 -- Index_Type with one more element at the low end of the range.
|
|
|
48 -- This type is never used but it forces GNATprove to check that there is
|
|
|
49 -- room for one more element at the low end of Index_Type.
|
|
|
50
|
|
|
51 type Sequence is private
|
|
|
52 with Default_Initial_Condition => Length (Sequence) = 0,
|
|
|
53 Iterable => (First => Iter_First,
|
|
|
54 Has_Element => Iter_Has_Element,
|
|
|
55 Next => Iter_Next,
|
|
|
56 Element => Get);
|
|
|
57 -- Sequences are empty when default initialized.
|
|
|
58 -- Quantification over sequences can be done using the regular
|
|
|
59 -- quantification over its range or directly on its elements with "for of".
|
|
|
60
|
|
|
61 -----------------------
|
|
|
62 -- Basic operations --
|
|
|
63 -----------------------
|
|
|
64
|
|
|
65 -- Sequences are axiomatized using Length and Get, providing respectively
|
|
|
66 -- the length of a sequence and an accessor to its Nth element:
|
|
|
67
|
|
|
68 function Length (Container : Sequence) return Count_Type with
|
|
|
69 -- Length of a sequence
|
|
|
70
|
|
|
71 Global => null,
|
|
|
72 Post =>
|
|
|
73 (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
|
|
|
74 Index_Type'Pos (Index_Type'Last);
|
|
|
75
|
|
|
76 function Get
|
|
|
77 (Container : Sequence;
|
|
|
78 Position : Extended_Index) return Element_Type
|
|
|
79 -- Access the Element at position Position in Container
|
|
|
80
|
|
|
81 with
|
|
|
82 Global => null,
|
|
|
83 Pre => Position in Index_Type'First .. Last (Container);
|
|
|
84
|
|
|
85 function Last (Container : Sequence) return Extended_Index with
|
|
|
86 -- Last index of a sequence
|
|
|
87
|
|
|
88 Global => null,
|
|
|
89 Post =>
|
|
|
90 Last'Result =
|
|
|
91 Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) +
|
|
|
92 Length (Container));
|
|
|
93 pragma Annotate (GNATprove, Inline_For_Proof, Last);
|
|
|
94
|
|
|
95 function First return Extended_Index is (Index_Type'First);
|
|
|
96 -- First index of a sequence
|
|
|
97
|
|
|
98 ------------------------
|
|
|
99 -- Property Functions --
|
|
|
100 ------------------------
|
|
|
101
|
|
|
102 function "=" (Left : Sequence; Right : Sequence) return Boolean with
|
|
|
103 -- Extensional equality over sequences
|
|
|
104
|
|
|
105 Global => null,
|
|
|
106 Post =>
|
|
|
107 "="'Result =
|
|
|
108 (Length (Left) = Length (Right)
|
|
|
109 and then (for all N in Index_Type'First .. Last (Left) =>
|
|
|
110 Get (Left, N) = Get (Right, N)));
|
|
|
111 pragma Annotate (GNATprove, Inline_For_Proof, "=");
|
|
|
112
|
|
|
113 function "<" (Left : Sequence; Right : Sequence) return Boolean with
|
|
|
114 -- Left is a strict subsequence of Right
|
|
|
115
|
|
|
116 Global => null,
|
|
|
117 Post =>
|
|
|
118 "<"'Result =
|
|
|
119 (Length (Left) < Length (Right)
|
|
|
120 and then (for all N in Index_Type'First .. Last (Left) =>
|
|
|
121 Get (Left, N) = Get (Right, N)));
|
|
|
122 pragma Annotate (GNATprove, Inline_For_Proof, "<");
|
|
|
123
|
|
|
124 function "<=" (Left : Sequence; Right : Sequence) return Boolean with
|
|
|
125 -- Left is a subsequence of Right
|
|
|
126
|
|
|
127 Global => null,
|
|
|
128 Post =>
|
|
|
129 "<="'Result =
|
|
|
130 (Length (Left) <= Length (Right)
|
|
|
131 and then (for all N in Index_Type'First .. Last (Left) =>
|
|
|
132 Get (Left, N) = Get (Right, N)));
|
|
|
133 pragma Annotate (GNATprove, Inline_For_Proof, "<=");
|
|
|
134
|
|
|
135 function Contains
|
|
|
136 (Container : Sequence;
|
|
|
137 Fst : Index_Type;
|
|
|
138 Lst : Extended_Index;
|
|
|
139 Item : Element_Type) return Boolean
|
|
|
140 -- Returns True if Item occurs in the range from Fst to Lst of Container
|
|
|
141
|
|
|
142 with
|
|
|
143 Global => null,
|
|
|
144 Pre => Lst <= Last (Container),
|
|
|
145 Post =>
|
|
|
146 Contains'Result =
|
|
|
147 (for some I in Fst .. Lst => Get (Container, I) = Item);
|
|
|
148 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
|
|
|
149
|
|
|
150 function Constant_Range
|
|
|
151 (Container : Sequence;
|
|
|
152 Fst : Index_Type;
|
|
|
153 Lst : Extended_Index;
|
|
|
154 Item : Element_Type) return Boolean
|
|
|
155 -- Returns True if every element of the range from Fst to Lst of Container
|
|
|
156 -- is equal to Item.
|
|
|
157
|
|
|
158 with
|
|
|
159 Global => null,
|
|
|
160 Pre => Lst <= Last (Container),
|
|
|
161 Post =>
|
|
|
162 Constant_Range'Result =
|
|
|
163 (for all I in Fst .. Lst => Get (Container, I) = Item);
|
|
|
164 pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
|
|
|
165
|
|
|
166 function Equal_Except
|
|
|
167 (Left : Sequence;
|
|
|
168 Right : Sequence;
|
|
|
169 Position : Index_Type) return Boolean
|
|
|
170 -- Returns True is Left and Right are the same except at position Position
|
|
|
171
|
|
|
172 with
|
|
|
173 Global => null,
|
|
|
174 Pre => Position <= Last (Left),
|
|
|
175 Post =>
|
|
|
176 Equal_Except'Result =
|
|
|
177 (Length (Left) = Length (Right)
|
|
|
178 and then (for all I in Index_Type'First .. Last (Left) =>
|
|
|
179 (if I /= Position then Get (Left, I) = Get (Right, I))));
|
|
|
180 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
|
|
|
181
|
|
|
182 function Equal_Except
|
|
|
183 (Left : Sequence;
|
|
|
184 Right : Sequence;
|
|
|
185 X : Index_Type;
|
|
|
186 Y : Index_Type) return Boolean
|
|
|
187 -- Returns True is Left and Right are the same except at positions X and Y
|
|
|
188
|
|
|
189 with
|
|
|
190 Global => null,
|
|
|
191 Pre => X <= Last (Left) and Y <= Last (Left),
|
|
|
192 Post =>
|
|
|
193 Equal_Except'Result =
|
|
|
194 (Length (Left) = Length (Right)
|
|
|
195 and then (for all I in Index_Type'First .. Last (Left) =>
|
|
|
196 (if I /= X and I /= Y then
|
|
|
197 Get (Left, I) = Get (Right, I))));
|
|
|
198 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
|
|
|
199
|
|
|
200 function Range_Equal
|
|
|
201 (Left : Sequence;
|
|
|
202 Right : Sequence;
|
|
|
203 Fst : Index_Type;
|
|
|
204 Lst : Extended_Index) return Boolean
|
|
|
205 -- Returns True if the ranges from Fst to Lst contain the same elements in
|
|
|
206 -- Left and Right.
|
|
|
207
|
|
|
208 with
|
|
|
209 Global => null,
|
|
|
210 Pre => Lst <= Last (Left) and Lst <= Last (Right),
|
|
|
211 Post =>
|
|
|
212 Range_Equal'Result =
|
|
|
213 (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I));
|
|
|
214 pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
|
|
|
215
|
|
|
216 function Range_Shifted
|
|
|
217 (Left : Sequence;
|
|
|
218 Right : Sequence;
|
|
|
219 Fst : Index_Type;
|
|
|
220 Lst : Extended_Index;
|
|
|
221 Offset : Count_Type'Base) return Boolean
|
|
|
222 -- Returns True if the range from Fst to Lst in Left contains the same
|
|
|
223 -- elements as the range from Fst + Offset to Lst + Offset in Right.
|
|
|
224
|
|
|
225 with
|
|
|
226 Global => null,
|
|
|
227 Pre =>
|
|
|
228 Lst <= Last (Left)
|
|
|
229 and then
|
|
|
230 (if Offset < 0 then
|
|
|
231 Index_Type'Pos (Index_Type'Base'First) - Offset <=
|
|
|
232 Index_Type'Pos (Index_Type'First))
|
|
|
233 and then
|
|
|
234 (if Fst <= Lst then
|
|
|
235 Offset in
|
|
|
236 Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
|
|
|
237 (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
|
|
|
238 Index_Type'Pos (Lst)),
|
|
|
239 Post =>
|
|
|
240 Range_Shifted'Result =
|
|
|
241 ((for all I in Fst .. Lst =>
|
|
|
242 Get (Left, I) =
|
|
|
243 Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)))
|
|
|
244 and
|
|
|
245 (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) ..
|
|
|
246 Index_Type'Val (Index_Type'Pos (Lst) + Offset)
|
|
|
247 =>
|
|
|
248 Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) =
|
|
|
249 Get (Right, I)));
|
|
|
250 pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
|
|
|
251
|
|
|
252 ----------------------------
|
|
|
253 -- Construction Functions --
|
|
|
254 ----------------------------
|
|
|
255
|
|
|
256 -- For better efficiency of both proofs and execution, avoid using
|
|
|
257 -- construction functions in annotations and rather use property functions.
|
|
|
258
|
|
|
259 function Set
|
|
|
260 (Container : Sequence;
|
|
|
261 Position : Index_Type;
|
|
|
262 New_Item : Element_Type) return Sequence
|
|
|
263 -- Returns a new sequence which contains the same elements as Container
|
|
|
264 -- except for the one at position Position which is replaced by New_Item.
|
|
|
265
|
|
|
266 with
|
|
|
267 Global => null,
|
|
|
268 Pre => Position in Index_Type'First .. Last (Container),
|
|
|
269 Post =>
|
|
|
270 Get (Set'Result, Position) = New_Item
|
|
|
271 and then Equal_Except (Container, Set'Result, Position);
|
|
|
272
|
|
|
273 function Add (Container : Sequence; New_Item : Element_Type) return Sequence
|
|
|
274 -- Returns a new sequence which contains the same elements as Container
|
|
|
275 -- plus New_Item at the end.
|
|
|
276
|
|
|
277 with
|
|
|
278 Global => null,
|
|
|
279 Pre =>
|
|
|
280 Length (Container) < Count_Type'Last
|
|
|
281 and then Last (Container) < Index_Type'Last,
|
|
|
282 Post =>
|
|
|
283 Length (Add'Result) = Length (Container) + 1
|
|
|
284 and then Get (Add'Result, Last (Add'Result)) = New_Item
|
|
|
285 and then Container <= Add'Result;
|
|
|
286
|
|
|
287 function Add
|
|
|
288 (Container : Sequence;
|
|
|
289 Position : Index_Type;
|
|
|
290 New_Item : Element_Type) return Sequence
|
|
|
291 with
|
|
|
292 -- Returns a new sequence which contains the same elements as Container
|
|
|
293 -- except that New_Item has been inserted at position Position.
|
|
|
294
|
|
|
295 Global => null,
|
|
|
296 Pre =>
|
|
|
297 Length (Container) < Count_Type'Last
|
|
|
298 and then Last (Container) < Index_Type'Last
|
|
|
299 and then Position <= Extended_Index'Succ (Last (Container)),
|
|
|
300 Post =>
|
|
|
301 Length (Add'Result) = Length (Container) + 1
|
|
|
302 and then Get (Add'Result, Position) = New_Item
|
|
|
303 and then Range_Equal
|
|
|
304 (Left => Container,
|
|
|
305 Right => Add'Result,
|
|
|
306 Fst => Index_Type'First,
|
|
|
307 Lst => Index_Type'Pred (Position))
|
|
|
308 and then Range_Shifted
|
|
|
309 (Left => Container,
|
|
|
310 Right => Add'Result,
|
|
|
311 Fst => Position,
|
|
|
312 Lst => Last (Container),
|
|
|
313 Offset => 1);
|
|
|
314
|
|
|
315 function Remove
|
|
|
316 (Container : Sequence;
|
|
|
317 Position : Index_Type) return Sequence
|
|
|
318 -- Returns a new sequence which contains the same elements as Container
|
|
|
319 -- except that the element at position Position has been removed.
|
|
|
320
|
|
|
321 with
|
|
|
322 Global => null,
|
|
|
323 Pre => Position in Index_Type'First .. Last (Container),
|
|
|
324 Post =>
|
|
|
325 Length (Remove'Result) = Length (Container) - 1
|
|
|
326 and then Range_Equal
|
|
|
327 (Left => Container,
|
|
|
328 Right => Remove'Result,
|
|
|
329 Fst => Index_Type'First,
|
|
|
330 Lst => Index_Type'Pred (Position))
|
|
|
331 and then Range_Shifted
|
|
|
332 (Left => Remove'Result,
|
|
|
333 Right => Container,
|
|
|
334 Fst => Position,
|
|
|
335 Lst => Last (Remove'Result),
|
|
|
336 Offset => 1);
|
|
|
337
|
|
|
338 ---------------------------
|
|
|
339 -- Iteration Primitives --
|
|
|
340 ---------------------------
|
|
|
341
|
|
|
342 function Iter_First (Container : Sequence) return Extended_Index with
|
|
|
343 Global => null;
|
|
|
344
|
|
|
345 function Iter_Has_Element
|
|
|
346 (Container : Sequence;
|
|
|
347 Position : Extended_Index) return Boolean
|
|
|
348 with
|
|
|
349 Global => null,
|
|
|
350 Post =>
|
|
|
351 Iter_Has_Element'Result =
|
|
|
352 (Position in Index_Type'First .. Last (Container));
|
|
|
353 pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
|
|
|
354
|
|
|
355 function Iter_Next
|
|
|
356 (Container : Sequence;
|
|
|
357 Position : Extended_Index) return Extended_Index
|
|
|
358 with
|
|
|
359 Global => null,
|
|
|
360 Pre => Iter_Has_Element (Container, Position);
|
|
|
361
|
|
|
362 private
|
|
|
363
|
|
|
364 pragma SPARK_Mode (Off);
|
|
|
365
|
|
|
366 package Containers is new Ada.Containers.Functional_Base
|
|
|
367 (Index_Type => Index_Type,
|
|
|
368 Element_Type => Element_Type);
|
|
|
369
|
|
|
370 type Sequence is record
|
|
|
371 Content : Containers.Container;
|
|
|
372 end record;
|
|
|
373
|
|
|
374 function Iter_First (Container : Sequence) return Extended_Index is
|
|
|
375 (Index_Type'First);
|
|
|
376
|
|
|
377 function Iter_Next
|
|
|
378 (Container : Sequence;
|
|
|
379 Position : Extended_Index) return Extended_Index
|
|
|
380 is
|
|
|
381 (if Position = Extended_Index'Last then
|
|
|
382 Extended_Index'First
|
|
|
383 else
|
|
|
384 Extended_Index'Succ (Position));
|
|
|
385
|
|
|
386 function Iter_Has_Element
|
|
|
387 (Container : Sequence;
|
|
|
388 Position : Extended_Index) return Boolean
|
|
|
389 is
|
|
|
390 (Position in Index_Type'First ..
|
|
|
391 (Index_Type'Val
|
|
|
392 ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))));
|
|
|
393
|
|
|
394 end Ada.Containers.Functional_Vectors;
|
