File : a-cfinve.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2014-2015, 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 -- --
23 -- --
24 -- --
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). In
34 -- addition, this is simplified by removing less-used functionality.
35
36 with Ada.Containers.Bounded_Holders;
37 with Ada.Containers.Formal_Vectors;
38
39 generic
40 type Index_Type is range <>;
41 type Element_Type (<>) is private;
42 Max_Size_In_Storage_Elements : Natural :=
43 Element_Type'Max_Size_In_Storage_Elements;
44 -- Maximum size of Vector elements in bytes. This has the same meaning as
45 -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
46 -- setting this too small can lead to erroneous execution; see comments in
47 -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
48 -- responsibility of clients to calculate the maximum size of all types in
49 -- the class.
50
51 with function "=" (Left, Right : Element_Type) return Boolean is <>;
52
53 Bounded : Boolean := True;
54 -- If True, the containers are bounded; the initial capacity is the maximum
55 -- size, and heap allocation will be avoided. If False, the containers can
56 -- grow via heap allocation.
57
58 package Ada.Containers.Formal_Indefinite_Vectors with
59 SPARK_Mode => On
60 is
61 pragma Annotate (GNATprove, External_Axiomatization);
62 pragma Annotate (CodePeer, Skip_Analysis);
63
64 subtype Extended_Index is Index_Type'Base
65 range Index_Type'First - 1 ..
66 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
67
68 No_Index : constant Extended_Index := Extended_Index'First;
69
70 subtype Capacity_Range is
71 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
72
73 type Vector (Capacity : Capacity_Range) is limited private with
74 Default_Initial_Condition;
75
76 function Empty_Vector return Vector;
77
78 function "=" (Left, Right : Vector) return Boolean with
79 Global => null;
80
81 function To_Vector
82 (New_Item : Element_Type;
83 Length : Capacity_Range) return Vector
84 with
85 Global => null;
86
87 function Capacity (Container : Vector) return Capacity_Range with
88 Global => null,
89 Post => Capacity'Result >= Container.Capacity;
90
91 procedure Reserve_Capacity
92 (Container : in out Vector;
93 Capacity : Capacity_Range)
94 with
95 Global => null,
96 Pre => (if Bounded then Capacity <= Container.Capacity);
97
98 function Length (Container : Vector) return Capacity_Range with
99 Global => null;
100
101 function Is_Empty (Container : Vector) return Boolean with
102 Global => null;
103
104 procedure Clear (Container : in out Vector) with
105 Global => null;
106 -- Note that this reclaims storage in the unbounded case. You need to call
107 -- this before a container goes out of scope in order to avoid storage
108 -- leaks.
109
110 procedure Assign (Target : in out Vector; Source : Vector) with
111 Global => null,
112 Pre => (if Bounded then Length (Source) <= Target.Capacity);
113
114 function Copy
115 (Source : Vector;
116 Capacity : Capacity_Range := 0) return Vector
117 with
118 Global => null,
119 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
120
121 function Element
122 (Container : Vector;
123 Index : Index_Type) return Element_Type
124 with
125 Global => null,
126 Pre => Index in First_Index (Container) .. Last_Index (Container);
127
128 procedure Replace_Element
129 (Container : in out Vector;
130 Index : Index_Type;
131 New_Item : Element_Type)
132 with
133 Global => null,
134 Pre => Index in First_Index (Container) .. Last_Index (Container);
135
136 procedure Append
137 (Container : in out Vector;
138 New_Item : Vector)
139 with
140 Global => null,
141 Pre => (if Bounded
142 then Length (Container) + Length (New_Item) <=
143 Container.Capacity);
144
145 procedure Append
146 (Container : in out Vector;
147 New_Item : Element_Type)
148 with
149 Global => null,
150 Pre => (if Bounded
151 then Length (Container) < Container.Capacity);
152
153 procedure Delete_Last
154 (Container : in out Vector)
155 with
156 Global => null;
157
158 procedure Reverse_Elements (Container : in out Vector) with
159 Global => null;
160
161 procedure Swap (Container : in out Vector; I, J : Index_Type) with
162 Global => null,
163 Pre => I in First_Index (Container) .. Last_Index (Container)
164 and then J in First_Index (Container) .. Last_Index (Container);
165
166 function First_Index (Container : Vector) return Index_Type with
167 Global => null;
168
169 function First_Element (Container : Vector) return Element_Type with
170 Global => null,
171 Pre => not Is_Empty (Container);
172
173 function Last_Index (Container : Vector) return Extended_Index with
174 Global => null;
175
176 function Last_Element (Container : Vector) return Element_Type with
177 Global => null,
178 Pre => not Is_Empty (Container);
179
180 function Find_Index
181 (Container : Vector;
182 Item : Element_Type;
183 Index : Index_Type := Index_Type'First) return Extended_Index
184 with
185 Global => null;
186
187 function Reverse_Find_Index
188 (Container : Vector;
189 Item : Element_Type;
190 Index : Index_Type := Index_Type'Last) return Extended_Index
191 with
192 Global => null;
193
194 function Contains
195 (Container : Vector;
196 Item : Element_Type) return Boolean
197 with
198 Global => null;
199
200 function Has_Element
201 (Container : Vector; Position : Extended_Index) return Boolean with
202 Global => null;
203
204 generic
205 with function "<" (Left, Right : Element_Type) return Boolean is <>;
206 package Generic_Sorting with SPARK_Mode is
207
208 function Is_Sorted (Container : Vector) return Boolean with
209 Global => null;
210
211 procedure Sort (Container : in out Vector) with
212 Global => null;
213
214 end Generic_Sorting;
215
216 function First_To_Previous
217 (Container : Vector;
218 Current : Index_Type) return Vector
219 with
220 Ghost,
221 Global => null;
222
223 function Current_To_Last
224 (Container : Vector;
225 Current : Index_Type) return Vector
226 with
227 Ghost,
228 Global => null;
229
230 private
231 pragma SPARK_Mode (Off);
232
233 pragma Inline (First_Index);
234 pragma Inline (Last_Index);
235 pragma Inline (Element);
236 pragma Inline (First_Element);
237 pragma Inline (Last_Element);
238 pragma Inline (Replace_Element);
239 pragma Inline (Contains);
240
241 -- The implementation method is to instantiate Bounded_Holders to get a
242 -- definite type for Element_Type, and then use that Holder type to
243 -- instantiate Formal_Vectors. All the operations are just wrappers.
244
245 package Holders is new Bounded_Holders
246 (Element_Type, Max_Size_In_Storage_Elements, "=");
247 use Holders;
248
249 package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
250 use Def;
251
252 -- ????Assert that Def subtypes have the same range
253
254 type Vector (Capacity : Capacity_Range) is limited record
255 V : Def.Vector (Capacity);
256 end record;
257
258 function Empty_Vector return Vector is
259 ((Capacity => 0, V => Def.Empty_Vector));
260
261 end Ada.Containers.Formal_Indefinite_Vectors;