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