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-2018, 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
63 elsif Index_Type'Last < -1
64 or else Index_Type'Pos (Index_Type'First) >
65 Index_Type'Pos (Index_Type'Last) - Count_Type'Last
67 Index_Type'Pos (Index_Type'Last) -
68 Index_Type'Pos (Index_Type'First) + 1
71 -- Maximal capacity of any vector. It is the minimum of the size of the
72 -- index range and the last possible Count_Type.
74 subtype Capacity_Range is Count_Type range 0 .. Last_Count;
76 type Vector (Capacity : Capacity_Range) is limited private with
77 Default_Initial_Condition => Is_Empty (Vector);
78 -- In the bounded case, Capacity is the capacity of the container, which
79 -- never changes. In the unbounded case, Capacity is the initial capacity
80 -- of the container, and operations such as Reserve_Capacity and Append can
81 -- increase the capacity. The capacity never shrinks, except in the case of
84 -- Note that all objects of type Vector are constrained, including in the
85 -- unbounded case; you can't assign from one object to another if the
86 -- Capacity is different.
88 function Length (Container : Vector) return Capacity_Range with
90 Post => Length'Result <= Capacity (Container);
92 pragma Unevaluated_Use_Of_Old (Allow);
94 package Formal_Model with Ghost is
96 package M is new Ada.Containers.Functional_Vectors
97 (Index_Type => Index_Type,
98 Element_Type => Element_Type);
102 Right : M.Sequence) return Boolean renames M."=";
106 Right : M.Sequence) return Boolean renames M."<";
110 Right : M.Sequence) return Boolean renames M."<=";
112 function M_Elements_In_Union
113 (Container : M.Sequence;
115 Right : M.Sequence) return Boolean
116 -- The elements of Container are contained in either Left or Right
120 M_Elements_In_Union'Result =
121 (for all I in Index_Type'First .. M.Last (Container) =>
122 (for some J in Index_Type'First .. M.Last (Left) =>
123 Element (Container, I) = Element (Left, J))
124 or (for some J in Index_Type'First .. M.Last (Right) =>
125 Element (Container, I) = Element (Right, J)));
126 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
128 function M_Elements_Included
130 L_Fst : Index_Type := Index_Type'First;
131 L_Lst : Extended_Index;
133 R_Fst : Index_Type := Index_Type'First;
134 R_Lst : Extended_Index) return Boolean
135 -- The elements of the slice from L_Fst to L_Lst in Left are contained
136 -- in the slide from R_Fst to R_Lst in Right.
139 Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
141 M_Elements_Included'Result =
142 (for all I in L_Fst .. L_Lst =>
143 (for some J in R_Fst .. R_Lst =>
144 Element (Left, I) = Element (Right, J)));
145 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
147 function M_Elements_Reversed
149 Right : M.Sequence) return Boolean
150 -- Right is Left in reverse order
154 M_Elements_Reversed'Result =
155 (M.Length (Left) = M.Length (Right)
156 and (for all I in Index_Type'First .. M.Last (Left) =>
158 Element (Right, M.Last (Left) - I + 1))
159 and (for all I in Index_Type'First .. M.Last (Right) =>
161 Element (Left, M.Last (Left) - I + 1)));
162 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
164 function M_Elements_Swapped
168 Y : Index_Type) return Boolean
169 -- Elements stored at X and Y are reversed in Left and Right
172 Pre => X <= M.Last (Left) and Y <= M.Last (Left),
174 M_Elements_Swapped'Result =
175 (M.Length (Left) = M.Length (Right)
176 and Element (Left, X) = Element (Right, Y)
177 and Element (Left, Y) = Element (Right, X)
178 and M.Equal_Except (Left, Right, X, Y));
179 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
181 function Model (Container : Vector) return M.Sequence with
182 -- The high-level model of a vector is a sequence of elements. The
183 -- sequence really is similar to the vector itself. However, it is not
184 -- limited which allows usage of 'Old
and 'Loop_Entry attributes.
188 Post => M.Length (Model'Result) = Length (Container);
192 I : Index_Type) return Element_Type renames M.Get;
193 -- To improve readability of contracts, we rename the function used to
194 -- access an element in the model to Element.
199 function Empty_Vector return Vector with
201 Post => Length (Empty_Vector'Result) = 0;
203 function "=" (Left, Right : Vector) return Boolean with
205 Post => "="'Result
= (Model
(Left
) = Model
(Right
));
208 (New_Item
: Element_Type
;
209 Length
: Capacity_Range
) return Vector
213 Formal_Vectors
.Length
(To_Vector
'Result) = Length
215 (Container
=> Model
(To_Vector
'Result),
216 Fst
=> Index_Type
'First,
217 Lst
=> Last_Index
(To_Vector
'Result),
220 function Capacity
(Container
: Vector
) return Capacity_Range
with
227 Capacity_Range
'Last);
228 pragma Annotate
(GNATprove
, Inline_For_Proof
, Capacity
);
230 procedure Reserve_Capacity
231 (Container
: in out Vector
;
232 Capacity
: Capacity_Range
)
235 Pre
=> (if Bounded
then Capacity
<= Container
.Capacity
),
236 Post
=> Model
(Container
) = Model
(Container
)'Old;
238 function Is_Empty
(Container
: Vector
) return Boolean with
240 Post
=> Is_Empty
'Result = (Length
(Container
) = 0);
242 procedure Clear
(Container
: in out Vector
) with
244 Post
=> Length
(Container
) = 0;
245 -- Note that this reclaims storage in the unbounded case. You need to call
246 -- this before a container goes out of scope in order to avoid storage
247 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
249 procedure Assign
(Target
: in out Vector
; Source
: Vector
) with
251 Pre
=> (if Bounded
then Length
(Source
) <= Target
.Capacity
),
252 Post
=> Model
(Target
) = Model
(Source
);
256 Capacity
: Capacity_Range
:= 0) return Vector
259 Pre
=> (if Bounded
then (Capacity
= 0 or Length
(Source
) <= Capacity
)),
261 Model
(Copy
'Result) = Model
(Source
)
262 and (if Capacity
= 0 then
263 Copy
'Result.Capacity
= Length
(Source
)
265 Copy
'Result.Capacity
= Capacity
);
267 procedure Move
(Target
: in out Vector
; Source
: in out Vector
)
270 Pre
=> (if Bounded
then Length
(Source
) <= Capacity
(Target
)),
271 Post
=> Model
(Target
) = Model
(Source
)'Old and Length
(Source
) = 0;
275 Index
: Index_Type
) return Element_Type
278 Pre
=> Index
in First_Index
(Container
) .. Last_Index
(Container
),
279 Post
=> Element
'Result = Element
(Model
(Container
), Index
);
280 pragma Annotate
(GNATprove
, Inline_For_Proof
, Element
);
282 procedure Replace_Element
283 (Container
: in out Vector
;
285 New_Item
: Element_Type
)
288 Pre
=> Index
in First_Index
(Container
) .. Last_Index
(Container
),
290 Length
(Container
) = Length
(Container
)'Old
292 -- Container now has New_Item at index Index
294 and Element
(Model
(Container
), Index
) = New_Item
296 -- All other elements are preserved
299 (Left
=> Model
(Container
)'Old,
300 Right
=> Model
(Container
),
304 (Container
: in out Vector
;
305 Before
: Extended_Index
;
310 Length
(Container
) <= Capacity
(Container
) - Length
(New_Item
)
311 and (Before
in Index_Type
'First .. Last_Index
(Container
)
312 or (Before
/= No_Index
313 and then Before
- 1 = Last_Index
(Container
))),
315 Length
(Container
) = Length
(Container
)'Old + Length
(New_Item
)
317 -- Elements located before Before in Container are preserved
320 (Left
=> Model
(Container
)'Old,
321 Right
=> Model
(Container
),
322 Fst
=> Index_Type
'First,
325 -- Elements of New_Item are inserted at position Before
327 and (if Length
(New_Item
) > 0 then
329 (Left
=> Model
(New_Item
),
330 Right
=> Model
(Container
),
331 Fst
=> Index_Type
'First,
332 Lst
=> Last_Index
(New_Item
),
333 Offset
=> Count_Type
(Before
- Index_Type
'First)))
335 -- Elements located after Before in Container are shifted
338 (Left
=> Model
(Container
)'Old,
339 Right
=> Model
(Container
),
341 Lst
=> Last_Index
(Container
)'Old,
342 Offset
=> Length
(New_Item
));
345 (Container
: in out Vector
;
346 Before
: Extended_Index
;
347 New_Item
: Element_Type
)
351 Length
(Container
) < Capacity
(Container
)
352 and then (Before
in Index_Type
'First .. Last_Index
(Container
) + 1),
354 Length
(Container
) = Length
(Container
)'Old + 1
356 -- Elements located before Before in Container are preserved
359 (Left
=> Model
(Container
)'Old,
360 Right
=> Model
(Container
),
361 Fst
=> Index_Type
'First,
364 -- Container now has New_Item at index Before
366 and Element
(Model
(Container
), Before
) = New_Item
368 -- Elements located after Before in Container are shifted by 1
371 (Left
=> Model
(Container
)'Old,
372 Right
=> Model
(Container
),
374 Lst
=> Last_Index
(Container
)'Old,
378 (Container
: in out Vector
;
379 Before
: Extended_Index
;
380 New_Item
: Element_Type
;
385 Length
(Container
) <= Capacity
(Container
) - Count
386 and (Before
in Index_Type
'First .. Last_Index
(Container
)
387 or (Before
/= No_Index
388 and then Before
- 1 = Last_Index
(Container
))),
390 Length
(Container
) = Length
(Container
)'Old + Count
392 -- Elements located before Before in Container are preserved
395 (Left
=> Model
(Container
)'Old,
396 Right
=> Model
(Container
),
397 Fst
=> Index_Type
'First,
400 -- New_Item is inserted Count times at position Before
402 and (if Count
> 0 then
404 (Container
=> Model
(Container
),
406 Lst
=> Before
+ Index_Type
'Base (Count
- 1),
409 -- Elements located after Before in Container are shifted
412 (Left
=> Model
(Container
)'Old,
413 Right
=> Model
(Container
),
415 Lst
=> Last_Index
(Container
)'Old,
418 procedure Prepend
(Container
: in out Vector
; New_Item
: Vector
) with
420 Pre
=> Length
(Container
) <= Capacity
(Container
) - Length
(New_Item
),
422 Length
(Container
) = Length
(Container
)'Old + Length
(New_Item
)
424 -- Elements of New_Item are inserted at the beginning of Container
427 (Left
=> Model
(New_Item
),
428 Right
=> Model
(Container
),
429 Fst
=> Index_Type
'First,
430 Lst
=> Last_Index
(New_Item
))
432 -- Elements of Container are shifted
435 (Left
=> Model
(Container
)'Old,
436 Right
=> Model
(Container
),
437 Fst
=> Index_Type
'First,
438 Lst
=> Last_Index
(Container
)'Old,
439 Offset
=> Length
(New_Item
));
441 procedure Prepend
(Container
: in out Vector
; New_Item
: Element_Type
) with
443 Pre
=> Length
(Container
) < Capacity
(Container
),
445 Length
(Container
) = Length
(Container
)'Old + 1
447 -- Container now has New_Item at Index_Type'First
449 and Element
(Model
(Container
), Index_Type
'First) = New_Item
451 -- Elements of Container are shifted by 1
454 (Left
=> Model
(Container
)'Old,
455 Right
=> Model
(Container
),
456 Fst
=> Index_Type
'First,
457 Lst
=> Last_Index
(Container
)'Old,
461 (Container
: in out Vector
;
462 New_Item
: Element_Type
;
466 Pre
=> Length
(Container
) <= Capacity
(Container
) - Count
,
468 Length
(Container
) = Length
(Container
)'Old + Count
470 -- New_Item is inserted Count times at the beginning of Container
473 (Container
=> Model
(Container
),
474 Fst
=> Index_Type
'First,
475 Lst
=> Index_Type
'First + Index_Type
'Base (Count
- 1),
478 -- Elements of Container are shifted
481 (Left
=> Model
(Container
)'Old,
482 Right
=> Model
(Container
),
483 Fst
=> Index_Type
'First,
484 Lst
=> Last_Index
(Container
)'Old,
487 procedure Append
(Container
: in out Vector
; New_Item
: Vector
) with
490 Length
(Container
) <= Capacity
(Container
) - Length
(New_Item
),
492 Length
(Container
) = Length
(Container
)'Old + Length
(New_Item
)
494 -- The elements of Container are preserved
496 and Model
(Container
)'Old <= Model
(Container
)
498 -- Elements of New_Item are inserted at the end of Container
500 and (if Length
(New_Item
) > 0 then
502 (Left
=> Model
(New_Item
),
503 Right
=> Model
(Container
),
504 Fst
=> Index_Type
'First,
505 Lst
=> Last_Index
(New_Item
),
508 (Last_Index
(Container
)'Old - Index_Type
'First + 1)));
510 procedure Append
(Container
: in out Vector
; New_Item
: Element_Type
) with
512 Pre
=> Length
(Container
) < Capacity
(Container
),
514 Length
(Container
) = Length
(Container
)'Old + 1
516 -- Elements of Container are preserved
518 and Model
(Container
)'Old < Model
(Container
)
520 -- Container now has New_Item at the end of Container
523 (Model
(Container
), Last_Index
(Container
)'Old + 1) = New_Item
;
526 (Container
: in out Vector
;
527 New_Item
: Element_Type
;
531 Pre
=> Length
(Container
) <= Capacity
(Container
) - Count
,
533 Length
(Container
) = Length
(Container
)'Old + Count
535 -- Elements of Container are preserved
537 and Model
(Container
)'Old <= Model
(Container
)
539 -- New_Item is inserted Count times at the end of Container
541 and (if Count
> 0 then
543 (Container
=> Model
(Container
),
544 Fst
=> Last_Index
(Container
)'Old + 1,
546 Last_Index
(Container
)'Old + Index_Type
'Base (Count
),
549 procedure Delete
(Container
: in out Vector
; Index
: Extended_Index
) with
551 Pre
=> Index
in First_Index
(Container
) .. Last_Index
(Container
),
553 Length
(Container
) = Length
(Container
)'Old - 1
555 -- Elements located before Index in Container are preserved
558 (Left
=> Model
(Container
)'Old,
559 Right
=> Model
(Container
),
560 Fst
=> Index_Type
'First,
563 -- Elements located after Index in Container are shifted by 1
566 (Left
=> Model
(Container
),
567 Right
=> Model
(Container
)'Old,
569 Lst
=> Last_Index
(Container
),
573 (Container
: in out Vector
;
574 Index
: Extended_Index
;
579 Index
in First_Index
(Container
) .. Last_Index
(Container
),
581 Length
(Container
) in
582 Length
(Container
)'Old - Count
.. Length
(Container
)'Old
584 -- The elements of Container located before Index are preserved.
587 (Left
=> Model
(Container
)'Old,
588 Right
=> Model
(Container
),
589 Fst
=> Index_Type
'First,
594 -- All the elements after Position have been erased
596 (Length
(Container
) - Count
<= Count_Type
(Index
- Index_Type
'First) =>
597 Length
(Container
) = Count_Type
(Index
- Index_Type
'First),
600 Length
(Container
) = Length
(Container
)'Old - Count
602 -- Other elements are shifted by Count
605 (Left
=> Model
(Container
),
606 Right
=> Model
(Container
)'Old,
608 Lst
=> Last_Index
(Container
),
611 procedure Delete_First
(Container
: in out Vector
) with
613 Pre
=> Length
(Container
) > 0,
615 Length
(Container
) = Length
(Container
)'Old - 1
617 -- Elements of Container are shifted by 1
620 (Left
=> Model
(Container
),
621 Right
=> Model
(Container
)'Old,
622 Fst
=> Index_Type
'First,
623 Lst
=> Last_Index
(Container
),
626 procedure Delete_First
(Container
: in out Vector
; Count
: Count_Type
) with
630 -- All the elements of Container have been erased
632 (Length
(Container
) <= Count
=> Length
(Container
) = 0,
635 Length
(Container
) = Length
(Container
)'Old - Count
637 -- Elements of Container are shifted by Count
640 (Left
=> Model
(Container
),
641 Right
=> Model
(Container
)'Old,
642 Fst
=> Index_Type
'First,
643 Lst
=> Last_Index
(Container
),
646 procedure Delete_Last
(Container
: in out Vector
) with
648 Pre
=> Length
(Container
) > 0,
650 Length
(Container
) = Length
(Container
)'Old - 1
652 -- Elements of Container are preserved
654 and Model
(Container
) < Model
(Container
)'Old;
656 procedure Delete_Last
(Container
: in out Vector
; Count
: Count_Type
) with
660 -- All the elements after Position have been erased
662 (Length
(Container
) <= Count
=> Length
(Container
) = 0,
665 Length
(Container
) = Length
(Container
)'Old - Count
667 -- The elements of Container are preserved
669 and Model
(Container
) <= Model
(Container
)'Old);
671 procedure Reverse_Elements
(Container
: in out Vector
) with
673 Post
=> M_Elements_Reversed
(Model
(Container
)'Old, Model
(Container
));
676 (Container
: in out Vector
;
682 I
in First_Index
(Container
) .. Last_Index
(Container
)
683 and then J
in First_Index
(Container
) .. Last_Index
(Container
),
685 M_Elements_Swapped
(Model
(Container
)'Old, Model
(Container
), I
, J
);
687 function First_Index
(Container
: Vector
) return Index_Type
with
689 Post
=> First_Index
'Result = Index_Type
'First;
690 pragma Annotate
(GNATprove
, Inline_For_Proof
, First_Index
);
692 function First_Element
(Container
: Vector
) return Element_Type
with
694 Pre
=> not Is_Empty
(Container
),
696 First_Element
'Result = Element
(Model
(Container
), Index_Type
'First);
697 pragma Annotate
(GNATprove
, Inline_For_Proof
, First_Element
);
699 function Last_Index
(Container
: Vector
) return Extended_Index
with
701 Post
=> Last_Index
'Result = M
.Last
(Model
(Container
));
702 pragma Annotate
(GNATprove
, Inline_For_Proof
, Last_Index
);
704 function Last_Element
(Container
: Vector
) return Element_Type
with
706 Pre
=> not Is_Empty
(Container
),
708 Last_Element
'Result =
709 Element
(Model
(Container
), Last_Index
(Container
));
710 pragma Annotate
(GNATprove
, Inline_For_Proof
, Last_Element
);
715 Index
: Index_Type
:= Index_Type
'First) return Extended_Index
720 -- If Item is not contained in Container after Index, Find_Index
723 (Index
> Last_Index
(Container
)
724 or else not M
.Contains
725 (Container
=> Model
(Container
),
727 Lst
=> Last_Index
(Container
),
730 Find_Index
'Result = No_Index
,
732 -- Otherwise, Find_Index returns a valid index greater than Index
735 Find_Index
'Result in Index
.. Last_Index
(Container
)
737 -- The element at this index in Container is Item
739 and Element
(Model
(Container
), Find_Index
'Result) = Item
741 -- It is the first occurrence of Item after Index in Container
744 (Container
=> Model
(Container
),
746 Lst
=> Find_Index
'Result - 1,
749 function Reverse_Find_Index
752 Index
: Index_Type
:= Index_Type
'Last) return Extended_Index
757 -- If Item is not contained in Container before Index,
758 -- Reverse_Find_Index returns No_Index.
761 (Container
=> Model
(Container
),
762 Fst
=> Index_Type
'First,
763 Lst
=> (if Index
<= Last_Index
(Container
) then Index
764 else Last_Index
(Container
)),
767 Reverse_Find_Index
'Result = No_Index
,
769 -- Otherwise, Reverse_Find_Index returns a valid index smaller than
773 Reverse_Find_Index
'Result in Index_Type
'First .. Index
774 and Reverse_Find_Index
'Result <= Last_Index
(Container
)
776 -- The element at this index in Container is Item
778 and Element
(Model
(Container
), Reverse_Find_Index
'Result) = Item
780 -- It is the last occurrence of Item before Index in Container
783 (Container
=> Model
(Container
),
784 Fst
=> Reverse_Find_Index
'Result + 1,
786 (if Index
<= Last_Index
(Container
) then
789 Last_Index
(Container
)),
794 Item
: Element_Type
) return Boolean
800 (Container
=> Model
(Container
),
801 Fst
=> Index_Type
'First,
802 Lst
=> Last_Index
(Container
),
807 Position
: Extended_Index
) return Boolean
812 (Position
in Index_Type
'First .. Last_Index
(Container
));
813 pragma Annotate
(GNATprove
, Inline_For_Proof
, Has_Element
);
816 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
817 package Generic_Sorting
with SPARK_Mode
is
819 package Formal_Model
with Ghost
is
821 function M_Elements_Sorted
(Container
: M
.Sequence
) return Boolean
825 M_Elements_Sorted
'Result =
826 (for all I
in Index_Type
'First .. M
.Last
(Container
) =>
827 (for all J
in I
.. M
.Last
(Container
) =>
828 Element
(Container
, I
) = Element
(Container
, J
)
829 or Element
(Container
, I
) < Element
(Container
, J
)));
830 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
845 (Left
=> Model
(Container
)'Old,
846 L_Lst
=> Last_Index
(Container
),
847 Right
=> Model
(Container
),
848 R_Lst
=> Last_Index
(Container
))
849 and M_Elements_Included
850 (Left
=> Model
(Container
),
851 L_Lst
=> Last_Index
(Container
),
852 Right
=> Model
(Container
)'Old,
853 R_Lst
=> Last_Index
(Container
));
855 procedure Merge
(Target
: in out Vector
; Source
: in out Vector
) with
856 -- Target and Source should not be aliased
858 Pre
=> Length
(Source
) <= Capacity
(Target
) - Length
(Target
),
860 Length
(Target
) = Length
(Target
)'Old + Length
(Source
)'Old
861 and Length
(Source
) = 0
862 and (if M_Elements_Sorted
(Model
(Target
)'Old)
863 and M_Elements_Sorted
(Model
(Source
)'Old)
865 M_Elements_Sorted
(Model
(Target
)))
866 and M_Elements_Included
867 (Left
=> Model
(Target
)'Old,
868 L_Lst
=> Last_Index
(Target
)'Old,
869 Right
=> Model
(Target
),
870 R_Lst
=> Last_Index
(Target
))
871 and M_Elements_Included
872 (Left
=> Model
(Source
)'Old,
873 L_Lst
=> Last_Index
(Source
)'Old,
874 Right
=> Model
(Target
),
875 R_Lst
=> Last_Index
(Target
))
876 and M_Elements_In_Union
883 pragma SPARK_Mode
(Off
);
885 pragma Inline
(First_Index
);
886 pragma Inline
(Last_Index
);
887 pragma Inline
(Element
);
888 pragma Inline
(First_Element
);
889 pragma Inline
(Last_Element
);
890 pragma Inline
(Replace_Element
);
891 pragma Inline
(Contains
);
893 subtype Array_Index
is Capacity_Range
range 1 .. Capacity_Range
'Last;
894 type Elements_Array
is array (Array_Index
range <>) of Element_Type
;
895 function "=" (L
, R
: Elements_Array
) return Boolean is abstract;
897 type Elements_Array_Ptr
is access all Elements_Array
;
899 type Vector
(Capacity
: Capacity_Range
) is limited record
901 -- In the bounded case, the elements are stored in Elements. In the
902 -- unbounded case, the elements are initially stored in Elements, until
903 -- we run out of room, then we switch to Elements_Ptr.
905 Last
: Extended_Index
:= No_Index
;
906 Elements_Ptr
: Elements_Array_Ptr
:= null;
907 Elements
: aliased Elements_Array
(1 .. Capacity
);
910 -- The primary reason Vector is limited is that in the unbounded case, once
911 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
912 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
913 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would
914 -- allow SPARK to "prove" things that are false. We could fix that by
915 -- making Vector a controlled type, and override Adjust to make a deep
916 -- copy, but finalization is not allowed in SPARK.
918 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
919 -- allowed on Vectors.
921 function Empty_Vector
return Vector
is
922 ((Capacity
=> 0, others => <>));
924 end Ada
.Containers
.Formal_Vectors
;