1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
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 --
9 -- Copyright (C) 2004-2017, Free Software Foundation, Inc. --
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. --
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. --
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. --
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 ------------------------------------------------------------------------------
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.
38 with Ada.Containers.Functional_Vectors;
41 type Index_Type is range <>;
42 type Element_Type is private;
44 Bounded : Boolean := True;
45 -- If True, the containers are bounded; the initial capacity is the maximum
46 -- size, and heap allocation will be avoided. If False, the containers can
47 -- grow via heap allocation.
49 package Ada.Containers.Formal_Vectors with
52 pragma Annotate (CodePeer, Skip_Analysis);
54 subtype Extended_Index is Index_Type'Base
55 range Index_Type'First - 1 ..
56 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
58 No_Index : constant Extended_Index := Extended_Index'First;
60 Last_Count : constant Count_Type :=
61 (if Index_Type'Last < Index_Type'First then 0
62 elsif Index_Type'Last < -1
63 or else Index_Type'Pos (Index_Type'First) >
64 Index_Type'Pos (Index_Type'Last) - Count_Type'Last
65 then Index_Type'Pos (Index_Type'Last) -
66 Index_Type'Pos (Index_Type'First) + 1
67 else Count_Type'Last);
68 -- Maximal capacity of any vector. It is the minimum of the size of the
69 -- index range and the last possible Count_Type.
71 subtype Capacity_Range is Count_Type range 0 .. Last_Count;
73 type Vector (Capacity : Capacity_Range) is limited private with
74 Default_Initial_Condition => Is_Empty (Vector);
75 -- In the bounded case, Capacity is the capacity of the container, which
76 -- never changes. In the unbounded case, Capacity is the initial capacity
77 -- of the container, and operations such as Reserve_Capacity and Append can
78 -- increase the capacity. The capacity never shrinks, except in the case of
81 -- Note that all objects of type Vector are constrained, including in the
82 -- unbounded case; you can't assign from one object to another if the
83 -- Capacity is different.
85 function Length (Container : Vector) return Capacity_Range with
87 Post => Length'Result <= Capacity (Container);
89 pragma Unevaluated_Use_Of_Old (Allow);
91 package Formal_Model with Ghost is
93 package M is new Ada.Containers.Functional_Vectors
94 (Index_Type => Index_Type,
95 Element_Type => Element_Type);
99 Right : M.Sequence) return Boolean renames M."=";
103 Right : M.Sequence) return Boolean renames M."<";
107 Right : M.Sequence) return Boolean renames M."<=";
109 function M_Elements_In_Union
110 (Container : M.Sequence;
112 Right : M.Sequence) return Boolean
113 -- The elements of Container are contained in either Left or Right
117 M_Elements_In_Union'Result =
118 (for all I in Index_Type'First .. M.Last (Container) =>
119 (for some J in Index_Type'First .. M.Last (Left) =>
120 Element (Container, I) = Element (Left, J))
121 or (for some J in Index_Type'First .. M.Last (Right) =>
122 Element (Container, I) = Element (Right, J)));
123 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
125 function M_Elements_Included
127 L_Fst : Index_Type := Index_Type'First;
128 L_Lst : Extended_Index;
130 R_Fst : Index_Type := Index_Type'First;
131 R_Lst : Extended_Index) return Boolean
132 -- The elements of the slice from L_Fst to L_Lst in Left are contained
133 -- in the slide from R_Fst to R_Lst in Right.
136 Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
138 M_Elements_Included'Result =
139 (for all I in L_Fst .. L_Lst =>
140 (for some J in R_Fst .. R_Lst =>
141 Element (Left, I) = Element (Right, J)));
142 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
144 function M_Elements_Reversed
146 Right : M.Sequence) return Boolean
147 -- Right is Left in reverse order
151 M_Elements_Reversed'Result =
152 (M.Length (Left) = M.Length (Right)
153 and (for all I in Index_Type'First .. M.Last (Left) =>
155 Element (Right, M.Last (Left) - I + 1))
156 and (for all I in Index_Type'First .. M.Last (Right) =>
158 Element (Left, M.Last (Left) - I + 1)));
159 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
161 function M_Elements_Swapped
165 Y : Index_Type) return Boolean
166 -- Elements stored at X and Y are reversed in Left and Right
169 Pre => X <= M.Last (Left) and Y <= M.Last (Left),
171 M_Elements_Swapped'Result =
172 (M.Length (Left) = M.Length (Right)
173 and Element (Left, X) = Element (Right, Y)
174 and Element (Left, Y) = Element (Right, X)
175 and M.Equal_Except (Left, Right, X, Y));
176 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
178 function Model (Container : Vector) return M.Sequence with
179 -- The high-level model of a vector is a sequence of elements. The
180 -- sequence really is similar to the vector itself. However, it is not
181 -- limited which allows usage of 'Old and 'Loop_Entry attributes.
185 Post => M.Length (Model'Result) = Length (Container);
189 I : Index_Type) return Element_Type renames M.Get;
190 -- To improve readability of contracts, we rename the function used to
191 -- access an element in the model to Element.
195 function Empty_Vector return Vector with
197 Post => Length (Empty_Vector'Result) = 0;
199 function "=" (Left, Right : Vector) return Boolean with
201 Post => "="'Result = (Model (Left) = Model (Right));
204 (New_Item : Element_Type;
205 Length : Capacity_Range) return Vector
209 Formal_Vectors.Length (To_Vector'Result) = Length
210 and M.Constant_Range (Container => Model (To_Vector'Result),
211 Fst => Index_Type'First,
212 Lst => Last_Index (To_Vector'Result),
215 function Capacity (Container : Vector) return Capacity_Range with
218 Capacity'Result = (if Bounded then Container.Capacity
219 else Capacity_Range'Last);
220 pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
222 procedure Reserve_Capacity
223 (Container : in out Vector;
224 Capacity : Capacity_Range)
227 Pre => (if Bounded then Capacity <= Container.Capacity),
228 Post => Model (Container) = Model (Container)'Old;
230 function Is_Empty (Container : Vector) return Boolean with
232 Post => Is_Empty'Result = (Length (Container) = 0);
234 procedure Clear (Container : in out Vector) with
236 Post => Length (Container) = 0;
237 -- Note that this reclaims storage in the unbounded case. You need to call
238 -- this before a container goes out of scope in order to avoid storage
239 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
241 procedure Assign (Target : in out Vector; Source : Vector) with
243 Pre => (if Bounded then Length (Source) <= Target.Capacity),
244 Post => Model (Target) = Model (Source);
248 Capacity : Capacity_Range := 0) return Vector
251 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
253 Model (Copy'Result) = Model (Source)
254 and (if Capacity = 0 then Copy'Result.Capacity = Length (Source)
255 else Copy'Result.Capacity = Capacity);
257 procedure Move (Target : in out Vector; Source : in out Vector)
260 Pre => (if Bounded then Length (Source) <= Capacity (Target)),
261 Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
265 Index : Index_Type) return Element_Type
268 Pre => Index in First_Index (Container) .. Last_Index (Container),
269 Post => Element'Result = Element (Model (Container), Index);
270 pragma Annotate (GNATprove, Inline_For_Proof, Element);
272 procedure Replace_Element
273 (Container : in out Vector;
275 New_Item : Element_Type)
278 Pre => Index in First_Index (Container) .. Last_Index (Container),
280 Length (Container) = Length (Container)'Old
282 -- Container now has New_Item at index Index
284 and Element (Model (Container), Index) = New_Item
286 -- All other elements are preserved
289 (Left => Model (Container)'Old,
290 Right => Model (Container),
294 (Container : in out Vector;
295 Before : Extended_Index;
300 Length (Container) <= Capacity (Container) - Length (New_Item)
301 and (Before in Index_Type'First .. Last_Index (Container)
302 or (Before /= No_Index
303 and then Before - 1 = Last_Index (Container))),
305 Length (Container) = Length (Container)'Old + Length (New_Item)
307 -- Elements located before Before in Container are preserved
310 (Left => Model (Container)'Old,
311 Right => Model (Container),
312 Fst => Index_Type'First,
315 -- Elements of New_Item are inserted at position Before
317 and (if Length (New_Item) > 0 then
319 (Left => Model (New_Item),
320 Right => Model (Container),
321 Fst => Index_Type'First,
322 Lst => Last_Index (New_Item),
323 Offset => Count_Type (Before - Index_Type'First)))
325 -- Elements located after Before in Container are shifted
328 (Left => Model (Container)'Old,
329 Right => Model (Container),
331 Lst => Last_Index (Container)'Old,
332 Offset => Length (New_Item));
335 (Container : in out Vector;
336 Before : Extended_Index;
337 New_Item : Element_Type)
341 Length (Container) < Capacity (Container)
342 and then (Before in Index_Type'First .. Last_Index (Container) + 1),
344 Length (Container) = Length (Container)'Old + 1
346 -- Elements located before Before in Container are preserved
349 (Left => Model (Container)'Old,
350 Right => Model (Container),
351 Fst => Index_Type'First,
354 -- Container now has New_Item at index Before
356 and Element (Model (Container), Before) = New_Item
358 -- Elements located after Before in Container are shifted by 1
361 (Left => Model (Container)'Old,
362 Right => Model (Container),
364 Lst => Last_Index (Container)'Old,
368 (Container : in out Vector;
369 Before : Extended_Index;
370 New_Item : Element_Type;
375 Length (Container) <= Capacity (Container) - Count
376 and (Before in Index_Type'First .. Last_Index (Container)
377 or (Before /= No_Index
378 and then Before - 1 = Last_Index (Container))),
380 Length (Container) = Length (Container)'Old + Count
382 -- Elements located before Before in Container are preserved
385 (Left => Model (Container)'Old,
386 Right => Model (Container),
387 Fst => Index_Type'First,
390 -- New_Item is inserted Count times at position Before
392 and (if Count > 0 then
394 (Container => Model (Container),
396 Lst => Before + Index_Type'Base (Count - 1),
399 -- Elements located after Before in Container are shifted
402 (Left => Model (Container)'Old,
403 Right => Model (Container),
405 Lst => Last_Index (Container)'Old,
409 (Container : in out Vector;
413 Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
415 Length (Container) = Length (Container)'Old + Length (New_Item)
417 -- Elements of New_Item are inserted at the beginning of Container
420 (Left => Model (New_Item),
421 Right => Model (Container),
422 Fst => Index_Type'First,
423 Lst => Last_Index (New_Item))
425 -- Elements of Container are shifted
428 (Left => Model (Container)'Old,
429 Right => Model (Container),
430 Fst => Index_Type'First,
431 Lst => Last_Index (Container)'Old,
432 Offset => Length (New_Item));
435 (Container : in out Vector;
436 New_Item : Element_Type)
439 Pre => Length (Container) < Capacity (Container),
441 Length (Container) = Length (Container)'Old + 1
443 -- Container now has New_Item at Index_Type'First
445 and Element (Model (Container), Index_Type'First) = New_Item
447 -- Elements of Container are shifted by 1
450 (Left => Model (Container)'Old,
451 Right => Model (Container),
452 Fst => Index_Type'First,
453 Lst => Last_Index (Container)'Old,
457 (Container : in out Vector;
458 New_Item : Element_Type;
462 Pre => Length (Container) <= Capacity (Container) - Count,
464 Length (Container) = Length (Container)'Old + Count
466 -- New_Item is inserted Count times at the beginning of Container
469 (Container => Model (Container),
470 Fst => Index_Type'First,
471 Lst => Index_Type'First + Index_Type'Base (Count - 1),
474 -- Elements of Container are shifted
477 (Left => Model (Container)'Old,
478 Right => Model (Container),
479 Fst => Index_Type'First,
480 Lst => Last_Index (Container)'Old,
484 (Container : in out Vector;
489 Length (Container) <= Capacity (Container) - Length (New_Item),
491 Length (Container) = Length (Container)'Old + Length (New_Item)
493 -- The elements of Container are preserved
495 and Model (Container)'Old <= Model (Container)
497 -- Elements of New_Item are inserted at the end of Container
499 and (if Length (New_Item) > 0 then
501 (Left => Model (New_Item),
502 Right => Model (Container),
503 Fst => Index_Type'First,
504 Lst => Last_Index (New_Item),
507 (Last_Index (Container)'Old - Index_Type'First + 1)));
510 (Container : in out Vector;
511 New_Item : Element_Type)
514 Pre => Length (Container) < Capacity (Container),
516 Length (Container) = Length (Container)'Old + 1
518 -- Elements of Container are preserved
520 and Model (Container)'Old < Model (Container)
522 -- Container now has New_Item at the end of Container
525 (Model (Container), Last_Index (Container)'Old + 1) = New_Item;
528 (Container : in out Vector;
529 New_Item : Element_Type;
533 Pre => Length (Container) <= Capacity (Container) - Count,
535 Length (Container) = Length (Container)'Old + Count
537 -- Elements of Container are preserved
539 and Model (Container)'Old <= Model (Container)
541 -- New_Item is inserted Count times at the end of Container
543 and (if Count > 0 then
545 (Container => Model (Container),
546 Fst => Last_Index (Container)'Old + 1,
548 Last_Index (Container)'Old + Index_Type'Base (Count),
552 (Container : in out Vector;
553 Index : Extended_Index)
556 Pre => Index in First_Index (Container) .. Last_Index (Container),
558 Length (Container) = Length (Container)'Old - 1
560 -- Elements located before Index in Container are preserved
563 (Left => Model (Container)'Old,
564 Right => Model (Container),
565 Fst => Index_Type'First,
568 -- Elements located after Index in Container are shifted by 1
571 (Left => Model (Container),
572 Right => Model (Container)'Old,
574 Lst => Last_Index (Container),
578 (Container : in out Vector;
579 Index : Extended_Index;
584 Index in First_Index (Container) .. Last_Index (Container),
586 Length (Container) in
587 Length (Container)'Old - Count .. Length (Container)'Old
589 -- The elements of Container located before Index are preserved.
592 (Left => Model (Container)'Old,
593 Right => Model (Container),
594 Fst => Index_Type'First,
599 -- All the elements after Position have been erased
601 (Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
602 Length (Container) = Count_Type (Index - Index_Type'First),
605 Length (Container) = Length (Container)'Old - Count
607 -- Other elements are shifted by Count
610 (Left => Model (Container),
611 Right => Model (Container)'Old,
613 Lst => Last_Index (Container),
616 procedure Delete_First
617 (Container : in out Vector)
620 Pre => Length (Container) > 0,
622 Length (Container) = Length (Container)'Old - 1
624 -- Elements of Container are shifted by 1
627 (Left => Model (Container),
628 Right => Model (Container)'Old,
629 Fst => Index_Type'First,
630 Lst => Last_Index (Container),
633 procedure Delete_First
634 (Container : in out Vector;
640 -- All the elements of Container have been erased
642 (Length (Container) <= Count => Length (Container) = 0,
645 Length (Container) = Length (Container)'Old - Count
647 -- Elements of Container are shifted by Count
650 (Left => Model (Container),
651 Right => Model (Container)'Old,
652 Fst => Index_Type'First,
653 Lst => Last_Index (Container),
656 procedure Delete_Last
657 (Container : in out Vector)
660 Pre => Length (Container) > 0,
662 Length (Container) = Length (Container)'Old - 1
664 -- Elements of Container are preserved
666 and Model (Container) < Model (Container)'Old;
668 procedure Delete_Last
669 (Container : in out Vector;
675 -- All the elements after Position have been erased
677 (Length (Container) <= Count => Length (Container) = 0,
680 Length (Container) = Length (Container)'Old - Count
682 -- The elements of Container are preserved
684 and Model (Container) <= Model (Container)'Old);
686 procedure Reverse_Elements (Container : in out Vector) with
688 Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
690 procedure Swap (Container : in out Vector; I, J : Index_Type) with
692 Pre => I in First_Index (Container) .. Last_Index (Container)
693 and then J in First_Index (Container) .. Last_Index (Container),
695 M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
697 function First_Index (Container : Vector) return Index_Type with
699 Post => First_Index'Result = Index_Type'First;
700 pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
702 function First_Element (Container : Vector) return Element_Type with
704 Pre => not Is_Empty (Container),
706 First_Element'Result = Element (Model (Container), Index_Type'First);
707 pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
709 function Last_Index (Container : Vector) return Extended_Index with
711 Post => Last_Index'Result = M.Last (Model (Container));
712 pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
714 function Last_Element (Container : Vector) return Element_Type with
716 Pre => not Is_Empty (Container),
718 Last_Element'Result =
719 Element (Model (Container), Last_Index (Container));
720 pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
725 Index : Index_Type := Index_Type'First) return Extended_Index
730 -- If Item is not is not contained in Container after Index, Find_Index
733 (Index > Last_Index (Container)
734 or else not M.Contains
735 (Container => Model (Container),
737 Lst => Last_Index (Container),
740 Find_Index'Result = No_Index,
742 -- Otherwise, Find_Index returns a valid index greater than Index
745 Find_Index'Result in Index .. Last_Index (Container)
747 -- The element at this index in Container is Item
749 and Element (Model (Container), Find_Index'Result) = Item
751 -- It is the first occurrence of Item after Index in Container
754 (Container => Model (Container),
756 Lst => Find_Index'Result - 1,
759 function Reverse_Find_Index
762 Index : Index_Type := Index_Type'Last) return Extended_Index
767 -- If Item is not is not contained in Container before Index,
768 -- Reverse_Find_Index returns No_Index.
771 (Container => Model (Container),
772 Fst => Index_Type'First,
773 Lst => (if Index <= Last_Index (Container) then Index
774 else Last_Index (Container)),
777 Reverse_Find_Index'Result = No_Index,
779 -- Otherwise, Reverse_Find_Index returns a valid index smaller than
783 Reverse_Find_Index'Result in Index_Type'First .. Index
784 and Reverse_Find_Index'Result <= Last_Index (Container)
786 -- The element at this index in Container is Item
788 and Element (Model (Container), Reverse_Find_Index'Result) = Item
790 -- It is the last occurrence of Item before Index in Container
793 (Container => Model (Container),
794 Fst => Reverse_Find_Index'Result + 1,
796 (if Index <= Last_Index (Container) then Index
797 else Last_Index (Container)),
802 Item : Element_Type) return Boolean
806 Contains'Result = M.Contains (Container => Model (Container),
807 Fst => Index_Type'First,
808 Lst => Last_Index (Container),
813 Position : Extended_Index) return Boolean
818 (Position in Index_Type'First .. Last_Index (Container));
819 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
822 with function "<" (Left, Right : Element_Type) return Boolean is <>;
823 package Generic_Sorting with SPARK_Mode is
824 function M_Elements_Sorted (Container : M.Sequence) return Boolean with
828 M_Elements_Sorted'Result =
829 (for all I in Index_Type'First .. M.Last (Container) =>
830 (for all J in I .. M.Last (Container) =>
831 Element (Container, I) = Element (Container, J)
832 or Element (Container, I) < Element (Container, J)));
833 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
835 function Is_Sorted (Container : Vector) return Boolean with
837 Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
839 procedure Sort (Container : in out Vector) with
842 Length (Container) = Length (Container)'Old
843 and M_Elements_Sorted (Model (Container))
844 and M_Elements_Included (Left => Model (Container)'Old,
845 L_Lst => Last_Index (Container),
846 Right => Model (Container),
847 R_Lst => Last_Index (Container))
848 and M_Elements_Included (Left => Model (Container),
849 L_Lst => Last_Index (Container),
850 Right => Model (Container)'Old,
851 R_Lst => Last_Index (Container));
853 procedure Merge (Target : in out Vector; Source : in out Vector) with
854 -- Target and Source should not be aliased
856 Pre => Length (Source) <= Capacity (Target) - Length (Target),
858 Length (Target) = Length (Target)'Old + Length (Source)'Old
859 and Length (Source) = 0
860 and (if M_Elements_Sorted (Model (Target)'Old)
861 and M_Elements_Sorted (Model (Source)'Old)
862 then M_Elements_Sorted (Model (Target)))
863 and M_Elements_Included (Left => Model (Target)'Old,
864 L_Lst => Last_Index (Target)'Old,
865 Right => Model (Target),
866 R_Lst => Last_Index (Target))
867 and M_Elements_Included (Left => Model (Source)'Old,
868 L_Lst => Last_Index (Source)'Old,
869 Right => Model (Target),
870 R_Lst => Last_Index (Target))
871 and M_Elements_In_Union (Model (Target),
877 pragma SPARK_Mode (Off);
879 pragma Inline (First_Index);
880 pragma Inline (Last_Index);
881 pragma Inline (Element);
882 pragma Inline (First_Element);
883 pragma Inline (Last_Element);
884 pragma Inline (Replace_Element);
885 pragma Inline (Contains);
887 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
888 type Elements_Array is array (Array_Index range <>) of Element_Type;
889 function "=" (L, R : Elements_Array) return Boolean is abstract;
891 type Elements_Array_Ptr is access all Elements_Array;
893 type Vector (Capacity : Capacity_Range) is limited record
894 -- In the bounded case, the elements are stored in Elements. In the
895 -- unbounded case, the elements are initially stored in Elements, until
896 -- we run out of room, then we switch to Elements_Ptr.
897 Last : Extended_Index := No_Index;
898 Elements_Ptr : Elements_Array_Ptr := null;
899 Elements : aliased Elements_Array (1 .. Capacity);
902 -- The primary reason Vector is limited is that in the unbounded case, once
903 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
904 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
905 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would
906 -- allow SPARK to "prove" things that are false. We could fix that by
907 -- making Vector a controlled type, and override Adjust to make a deep
908 -- copy, but finalization is not allowed in SPARK.
910 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
911 -- allowed on Vectors.
913 function Empty_Vector return Vector is
914 ((Capacity => 0, others => <>));
916 end Ada.Containers.Formal_Vectors;