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 _ V E C T O R S        --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--          Copyright (C) 2004-2013, 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--  This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
33--  2012 RM. The modifications are meant to facilitate formal proofs by making
34--  it easier to express properties, and by making the specification of this
35--  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: Element, Next, Query_Element, Previous, Iterate,
42--    Has_Element, Reverse_Iterate. This change is motivated by the need
43--    to have cursors which are valid on different containers (typically a
44--    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.
47
48--    There are three new functions:
49
50--      function Strict_Equal (Left, Right : Vector) return Boolean;
51--      function First_To_Previous  (Container : Vector; Current : Cursor)
52--         return Vector;
53--      function Current_To_Last (Container : Vector; Current : Cursor)
54--         return Vector;
55
56--    See detailed specifications for these subprograms
57
58with Ada.Containers;
59use Ada.Containers;
60
61generic
62   type Index_Type is range <>;
63   type Element_Type is private;
64
65   with function "=" (Left, Right : Element_Type) return Boolean is <>;
66
67package Ada.Containers.Formal_Vectors is
68   pragma Annotate (GNATprove, External_Axiomatization);
69   pragma Pure;
70
71   subtype Extended_Index is Index_Type'Base
72   range Index_Type'First - 1 ..
73     Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
74
75   No_Index : constant Extended_Index := Extended_Index'First;
76
77   subtype Capacity_Range is
78     Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
79
80   type Vector (Capacity : Capacity_Range) is private with
81     Iterable => (First       => First,
82                  Next        => Next,
83                  Has_Element => Has_Element,
84                  Element     => Element);
85
86   type Cursor is private;
87   pragma Preelaborable_Initialization (Cursor);
88
89   Empty_Vector : constant Vector;
90
91   No_Element : constant Cursor;
92
93   function "=" (Left, Right : Vector) return Boolean with
94     Global => null;
95
96   function To_Vector
97     (New_Item : Element_Type;
98      Length   : Count_Type) return Vector
99   with
100     Global => null;
101
102   function "&" (Left, Right : Vector) return Vector with
103     Global => null,
104     Pre    => Capacity_Range'Last - Length (Left) >= Length (Right);
105
106   function "&" (Left : Vector; Right : Element_Type) return Vector with
107     Global => null,
108     Pre    => Length (Left) < Capacity_Range'Last;
109
110   function "&" (Left : Element_Type; Right : Vector) return Vector with
111     Global => null,
112     Pre    => Length (Right) < Capacity_Range'Last;
113
114   function "&" (Left, Right : Element_Type) return Vector with
115     Global => null,
116     Pre    => Capacity_Range'Last >= 2;
117
118   function Capacity (Container : Vector) return Count_Type with
119     Global => null;
120
121   procedure Reserve_Capacity
122     (Container : in out Vector;
123      Capacity  : Count_Type)
124   with
125     Global => null,
126     Pre    => Capacity <= Container.Capacity;
127
128   function Length (Container : Vector) return Count_Type with
129     Global => null;
130
131   procedure Set_Length
132     (Container : in out Vector;
133      New_Length    : Count_Type)
134   with
135     Global => null,
136     Pre    => New_Length <= Length (Container);
137
138   function Is_Empty (Container : Vector) return Boolean with
139     Global => null;
140
141   procedure Clear (Container : in out Vector) with
142     Global => null;
143
144   procedure Assign (Target : in out Vector; Source : Vector) with
145     Global => null,
146     Pre    => Length (Source) <= Target.Capacity;
147
148   function Copy
149     (Source   : Vector;
150      Capacity : Count_Type := 0) return Vector
151   with
152     Global => null,
153     Pre    => Length (Source) <= Capacity and then Capacity in Capacity_Range;
154
155   function To_Cursor
156     (Container : Vector;
157      Index     : Extended_Index) return Cursor
158   with
159     Global => null;
160
161   function To_Index (Position : Cursor) return Extended_Index with
162     Global => null;
163
164   function Element
165     (Container : Vector;
166      Index     : Index_Type) return Element_Type
167   with
168     Global => null,
169     Pre    => First_Index (Container) <= Index
170                 and then Index <= Last_Index (Container);
171
172   function Element
173     (Container : Vector;
174      Position  : Cursor) return Element_Type
175   with
176     Global => null,
177     Pre    => Has_Element (Container, Position);
178
179   procedure Replace_Element
180     (Container : in out Vector;
181      Index     : Index_Type;
182      New_Item  : Element_Type)
183   with
184     Global => null,
185     Pre    => First_Index (Container) <= Index
186                 and then Index <= Last_Index (Container);
187
188   procedure Replace_Element
189     (Container : in out Vector;
190      Position  : Cursor;
191      New_Item  : Element_Type)
192   with
193     Global => null,
194     Pre    => Has_Element (Container, Position);
195
196   procedure Move (Target : in out Vector; Source : in out Vector) with
197     Global => null,
198     Pre    => Length (Source) <= Target.Capacity;
199
200   procedure Insert
201     (Container : in out Vector;
202      Before    : Extended_Index;
203      New_Item  : Vector)
204   with
205     Global => null,
206     Pre    => First_Index (Container) <= Before
207                 and then Before <= Last_Index (Container) + 1
208                 and then Length (Container) < Container.Capacity;
209
210   procedure Insert
211     (Container : in out Vector;
212      Before    : Cursor;
213      New_Item  : Vector)
214   with
215     Global => null,
216     Pre    => Length (Container) < Container.Capacity
217                 and then (Has_Element (Container, Before)
218                            or else Before = No_Element);
219
220   procedure Insert
221     (Container : in out Vector;
222      Before    : Cursor;
223      New_Item  : Vector;
224      Position  : out Cursor)
225   with
226     Global => null,
227     Pre    => Length (Container) < Container.Capacity
228                 and then (Has_Element (Container, Before)
229                            or else Before = No_Element);
230
231   procedure Insert
232     (Container : in out Vector;
233      Before    : Extended_Index;
234      New_Item  : Element_Type;
235      Count     : Count_Type := 1)
236   with
237     Global => null,
238     Pre    => First_Index (Container) <= Before
239                 and then Before <= Last_Index (Container) + 1
240                 and then Length (Container) + Count <= Container.Capacity;
241
242   procedure Insert
243     (Container : in out Vector;
244      Before    : Cursor;
245      New_Item  : Element_Type;
246      Count     : Count_Type := 1)
247   with
248     Global => null,
249     Pre    => Length (Container) + Count <= Container.Capacity
250                 and then (Has_Element (Container, Before)
251                            or else Before = No_Element);
252
253   procedure Insert
254     (Container : in out Vector;
255      Before    : Cursor;
256      New_Item  : Element_Type;
257      Position  : out Cursor;
258      Count     : Count_Type := 1)
259   with
260     Global => null,
261     Pre    => Length (Container) + Count <= Container.Capacity
262                 and then (Has_Element (Container, Before)
263                            or else Before = No_Element);
264
265   procedure Prepend
266     (Container : in out Vector;
267      New_Item  : Vector)
268   with
269     Global => null,
270     Pre    => Length (Container) < Container.Capacity;
271
272   procedure Prepend
273     (Container : in out Vector;
274      New_Item  : Element_Type;
275      Count     : Count_Type := 1)
276   with
277     Global => null,
278     Pre    => Length (Container) + Count <= Container.Capacity;
279
280   procedure Append
281     (Container : in out Vector;
282      New_Item  : Vector)
283   with
284     Global => null,
285     Pre    => Length (Container) < Container.Capacity;
286
287   procedure Append
288     (Container : in out Vector;
289      New_Item  : Element_Type;
290      Count     : Count_Type := 1)
291   with
292     Global => null,
293     Pre    => Length (Container) + Count <= Container.Capacity;
294
295   procedure Delete
296     (Container : in out Vector;
297      Index     : Extended_Index;
298      Count     : Count_Type := 1)
299   with
300     Global => null,
301     Pre    => First_Index (Container) <= Index
302                 and then Index <= Last_Index (Container) + 1;
303
304   procedure Delete
305     (Container : in out Vector;
306      Position  : in out Cursor;
307      Count     : Count_Type := 1)
308   with
309     Global => null,
310     Pre    => Has_Element (Container, Position);
311
312   procedure Delete_First
313     (Container : in out Vector;
314      Count     : Count_Type := 1)
315   with
316     Global => null;
317
318   procedure Delete_Last
319     (Container : in out Vector;
320      Count     : Count_Type := 1)
321   with
322     Global => null;
323
324   procedure Reverse_Elements (Container : in out Vector) with
325     Global => null;
326
327   procedure Swap (Container : in out Vector; I, J : Index_Type) with
328     Global => null,
329     Pre    => First_Index (Container) <= I
330                 and then I <= Last_Index (Container)
331                 and then First_Index (Container) <= J
332                 and then J <= Last_Index (Container);
333
334   procedure Swap (Container : in out Vector; I, J : Cursor) with
335     Global => null,
336     Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
337
338   function First_Index (Container : Vector) return Index_Type with
339     Global => null;
340
341   function First (Container : Vector) return Cursor with
342     Global => null;
343
344   function First_Element (Container : Vector) return Element_Type with
345     Global => null,
346     Pre    => not Is_Empty (Container);
347
348   function Last_Index (Container : Vector) return Extended_Index with
349     Global => null;
350
351   function Last (Container : Vector) return Cursor with
352     Global => null;
353
354   function Last_Element (Container : Vector) return Element_Type with
355     Global => null,
356     Pre    => not Is_Empty (Container);
357
358   function Next (Container : Vector; Position : Cursor) return Cursor with
359     Global => null,
360     Pre    => Has_Element (Container, Position) or else Position = No_Element;
361
362   procedure Next (Container : Vector; Position : in out Cursor) with
363     Global => null,
364     Pre    => Has_Element (Container, Position) or else Position = No_Element;
365
366   function Previous (Container : Vector; Position : Cursor) return Cursor with
367     Global => null,
368     Pre    => Has_Element (Container, Position) or else Position = No_Element;
369
370   procedure Previous (Container : Vector; Position : in out Cursor) with
371     Global => null,
372     Pre    => Has_Element (Container, Position) or else Position = No_Element;
373
374   function Find_Index
375     (Container : Vector;
376      Item      : Element_Type;
377      Index     : Index_Type := Index_Type'First) return Extended_Index
378   with
379     Global => null;
380
381   function Find
382     (Container : Vector;
383      Item      : Element_Type;
384      Position  : Cursor := No_Element) return Cursor
385   with
386     Global => null,
387     Pre    => Has_Element (Container, Position) or else Position = No_Element;
388
389   function Reverse_Find_Index
390     (Container : Vector;
391      Item      : Element_Type;
392      Index     : Index_Type := Index_Type'Last) return Extended_Index
393   with
394     Global => null;
395
396   function Reverse_Find
397     (Container : Vector;
398      Item      : Element_Type;
399      Position  : Cursor := No_Element) return Cursor
400   with
401     Global => null,
402     Pre    => Has_Element (Container, Position) or else Position = No_Element;
403
404   function Contains
405     (Container : Vector;
406      Item      : Element_Type) return Boolean
407   with
408     Global => null;
409
410   function Has_Element (Container : Vector; Position : Cursor) return Boolean
411   with
412     Global => null;
413
414   generic
415      with function "<" (Left, Right : Element_Type) return Boolean is <>;
416   package Generic_Sorting is
417
418      function Is_Sorted (Container : Vector) return Boolean with
419        Global => null;
420
421      procedure Sort (Container : in out Vector) with
422        Global => null;
423
424      procedure Merge (Target : in out Vector; Source : in out Vector) with
425        Global => null;
426
427   end Generic_Sorting;
428
429   function Strict_Equal (Left, Right : Vector) return Boolean with
430     Global => null;
431   --  Strict_Equal returns True if the containers are physically equal, i.e.
432   --  they are structurally equal (function "=" returns True) and that they
433   --  have the same set of cursors.
434
435   function First_To_Previous
436     (Container : Vector;
437      Current : Cursor) return Vector
438   with
439     Global => null,
440     Pre    => Has_Element (Container, Current) or else Current = No_Element;
441   function Current_To_Last
442     (Container : Vector;
443      Current : Cursor) return Vector
444   with
445     Global => null,
446     Pre    => Has_Element (Container, Current) or else Current = No_Element;
447   --  First_To_Previous returns a container containing all elements preceding
448   --  Current (excluded) in Container. Current_To_Last returns a container
449   --  containing all elements following Current (included) in Container.
450   --  These two new functions can be used to express invariant properties in
451   --  loops which iterate over containers. First_To_Previous returns the part
452   --  of the container already scanned and Current_To_Last the part not
453   --  scanned yet.
454
455private
456
457   pragma Inline (First_Index);
458   pragma Inline (Last_Index);
459   pragma Inline (Element);
460   pragma Inline (First_Element);
461   pragma Inline (Last_Element);
462   pragma Inline (Replace_Element);
463   pragma Inline (Contains);
464   pragma Inline (Next);
465   pragma Inline (Previous);
466
467   type Elements_Array is array (Count_Type range <>) of Element_Type;
468   function "=" (L, R : Elements_Array) return Boolean is abstract;
469
470   type Vector (Capacity : Capacity_Range) is record
471      Elements : Elements_Array (1 .. Capacity);
472      Last     : Extended_Index := No_Index;
473   end record;
474
475   type Cursor is record
476      Valid : Boolean    := True;
477      Index : Index_Type := Index_Type'First;
478   end record;
479
480   Empty_Vector : constant Vector := (Capacity => 0, others => <>);
481
482   No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
483
484end Ada.Containers.Formal_Vectors;
485