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-2019, 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;
43 with function "=" (Left, Right : Element_Type) return Boolean is <>;
45 package Ada.Containers.Formal_Vectors with
48 pragma Annotate (CodePeer, Skip_Analysis);
50 subtype Extended_Index is Index_Type'Base
51 range Index_Type'First - 1 ..
52 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
54 No_Index : constant Extended_Index := Extended_Index'First;
56 Last_Count : constant Count_Type :=
57 (if Index_Type'Last < Index_Type'First then
59 elsif Index_Type'Last < -1
60 or else Index_Type'Pos (Index_Type'First) >
61 Index_Type'Pos (Index_Type'Last) - Count_Type'Last
63 Index_Type'Pos (Index_Type'Last) -
64 Index_Type'Pos (Index_Type'First) + 1
67 -- Maximal capacity of any vector. It is the minimum of the size of the
68 -- index range and the last possible Count_Type.
70 subtype Capacity_Range is Count_Type range 0 .. Last_Count;
72 type Vector (Capacity : Capacity_Range) is private with
73 Default_Initial_Condition => Is_Empty (Vector);
75 function Length (Container : Vector) return Capacity_Range with
77 Post => Length'Result <= Capacity (Container);
79 pragma Unevaluated_Use_Of_Old (Allow);
81 package Formal_Model with Ghost is
83 package M is new Ada.Containers.Functional_Vectors
84 (Index_Type => Index_Type,
85 Element_Type => Element_Type);
89 Right : M.Sequence) return Boolean renames M."=";
93 Right : M.Sequence) return Boolean renames M."<";
97 Right : M.Sequence) return Boolean renames M."<=";
99 function M_Elements_In_Union
100 (Container : M.Sequence;
102 Right : M.Sequence) return Boolean
103 -- The elements of Container are contained in either Left or Right
107 M_Elements_In_Union'Result =
108 (for all I in Index_Type'First .. M.Last (Container) =>
109 (for some J in Index_Type'First .. M.Last (Left) =>
110 Element (Container, I) = Element (Left, J))
111 or (for some J in Index_Type'First .. M.Last (Right) =>
112 Element (Container, I) = Element (Right, J)));
113 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
115 function M_Elements_Included
117 L_Fst : Index_Type := Index_Type'First;
118 L_Lst : Extended_Index;
120 R_Fst : Index_Type := Index_Type'First;
121 R_Lst : Extended_Index) return Boolean
122 -- The elements of the slice from L_Fst to L_Lst in Left are contained
123 -- in the slide from R_Fst to R_Lst in Right.
126 Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
128 M_Elements_Included'Result =
129 (for all I in L_Fst .. L_Lst =>
130 (for some J in R_Fst .. R_Lst =>
131 Element (Left, I) = Element (Right, J)));
132 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
134 function M_Elements_Reversed
136 Right : M.Sequence) return Boolean
137 -- Right is Left in reverse order
141 M_Elements_Reversed'Result =
142 (M.Length (Left) = M.Length (Right)
143 and (for all I in Index_Type'First .. M.Last (Left) =>
145 Element (Right, M.Last (Left) - I + 1))
146 and (for all I in Index_Type'First .. M.Last (Right) =>
148 Element (Left, M.Last (Left) - I + 1)));
149 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
151 function M_Elements_Swapped
155 Y : Index_Type) return Boolean
156 -- Elements stored at X and Y are reversed in Left and Right
159 Pre => X <= M.Last (Left) and Y <= M.Last (Left),
161 M_Elements_Swapped'Result =
162 (M.Length (Left) = M.Length (Right)
163 and Element (Left, X) = Element (Right, Y)
164 and Element (Left, Y) = Element (Right, X)
165 and M.Equal_Except (Left, Right, X, Y));
166 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
168 function Model (Container : Vector) return M.Sequence with
169 -- The high-level model of a vector is a sequence of elements. The
170 -- sequence really is similar to the vector itself. However, it is not
171 -- limited which allows usage of 'Old and 'Loop_Entry attributes.
175 Post => M.Length (Model'Result) = Length (Container);
179 I : Index_Type) return Element_Type renames M.Get;
180 -- To improve readability of contracts, we rename the function used to
181 -- access an element in the model to Element.
186 function Empty_Vector return Vector with
188 Post => Length (Empty_Vector'Result) = 0;
190 function "=" (Left, Right : Vector) return Boolean with
192 Post => "="'Result = (Model (Left) = Model (Right));
195 (New_Item : Element_Type;
196 Length : Capacity_Range) return Vector
200 Formal_Vectors.Length (To_Vector'Result) = Length
202 (Container => Model (To_Vector'Result),
203 Fst => Index_Type'First,
204 Lst => Last_Index (To_Vector'Result),
207 function Capacity (Container : Vector) return Capacity_Range with
210 Capacity'Result = Container.Capacity;
211 pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
213 procedure Reserve_Capacity
214 (Container : in out Vector;
215 Capacity : Capacity_Range)
218 Pre => Capacity <= Container.Capacity,
219 Post => Model (Container) = Model (Container)'Old;
221 function Is_Empty (Container : Vector) return Boolean with
223 Post => Is_Empty'Result = (Length (Container) = 0);
225 procedure Clear (Container : in out Vector) with
227 Post => Length (Container) = 0;
229 procedure Assign (Target : in out Vector; Source : Vector) with
231 Pre => Length (Source) <= Target.Capacity,
232 Post => Model (Target) = Model (Source);
236 Capacity : Capacity_Range := 0) return Vector
239 Pre => (Capacity = 0 or Length (Source) <= Capacity),
241 Model (Copy'Result) = Model (Source)
242 and (if Capacity = 0 then
243 Copy'Result.Capacity = Length (Source)
245 Copy'Result.Capacity = Capacity);
247 procedure Move (Target : in out Vector; Source : in out Vector)
250 Pre => Length (Source) <= Capacity (Target),
251 Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
255 Index : Index_Type) return Element_Type
258 Pre => Index in First_Index (Container) .. Last_Index (Container),
259 Post => Element'Result = Element (Model (Container), Index);
260 pragma Annotate (GNATprove, Inline_For_Proof, Element);
262 procedure Replace_Element
263 (Container : in out Vector;
265 New_Item : Element_Type)
268 Pre => Index in First_Index (Container) .. Last_Index (Container),
270 Length (Container) = Length (Container)'Old
272 -- Container now has New_Item at index Index
274 and Element (Model (Container), Index) = New_Item
276 -- All other elements are preserved
279 (Left => Model (Container)'Old,
280 Right => Model (Container),
284 (Container : in out Vector;
285 Before : Extended_Index;
290 Length (Container) <= Capacity (Container) - Length (New_Item)
291 and (Before in Index_Type'First .. Last_Index (Container)
292 or (Before /= No_Index
293 and then Before - 1 = Last_Index (Container))),
295 Length (Container) = Length (Container)'Old + Length (New_Item)
297 -- Elements located before Before in Container are preserved
300 (Left => Model (Container)'Old,
301 Right => Model (Container),
302 Fst => Index_Type'First,
305 -- Elements of New_Item are inserted at position Before
307 and (if Length (New_Item) > 0 then
309 (Left => Model (New_Item),
310 Right => Model (Container),
311 Fst => Index_Type'First,
312 Lst => Last_Index (New_Item),
313 Offset => Count_Type (Before - Index_Type'First)))
315 -- Elements located after Before in Container are shifted
318 (Left => Model (Container)'Old,
319 Right => Model (Container),
321 Lst => Last_Index (Container)'Old,
322 Offset => Length (New_Item));
325 (Container : in out Vector;
326 Before : Extended_Index;
327 New_Item : Element_Type)
331 Length (Container) < Capacity (Container)
332 and then (Before in Index_Type'First .. Last_Index (Container) + 1),
334 Length (Container) = Length (Container)'Old + 1
336 -- Elements located before Before in Container are preserved
339 (Left => Model (Container)'Old,
340 Right => Model (Container),
341 Fst => Index_Type'First,
344 -- Container now has New_Item at index Before
346 and Element (Model (Container), Before) = New_Item
348 -- Elements located after Before in Container are shifted by 1
351 (Left => Model (Container)'Old,
352 Right => Model (Container),
354 Lst => Last_Index (Container)'Old,
358 (Container : in out Vector;
359 Before : Extended_Index;
360 New_Item : Element_Type;
365 Length (Container) <= Capacity (Container) - Count
366 and (Before in Index_Type'First .. Last_Index (Container)
367 or (Before /= No_Index
368 and then Before - 1 = Last_Index (Container))),
370 Length (Container) = Length (Container)'Old + Count
372 -- Elements located before Before in Container are preserved
375 (Left => Model (Container)'Old,
376 Right => Model (Container),
377 Fst => Index_Type'First,
380 -- New_Item is inserted Count times at position Before
382 and (if Count > 0 then
384 (Container => Model (Container),
386 Lst => Before + Index_Type'Base (Count - 1),
389 -- Elements located after Before in Container are shifted
392 (Left => Model (Container)'Old,
393 Right => Model (Container),
395 Lst => Last_Index (Container)'Old,
398 procedure Prepend (Container : in out Vector; New_Item : Vector) with
400 Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
402 Length (Container) = Length (Container)'Old + Length (New_Item)
404 -- Elements of New_Item are inserted at the beginning of Container
407 (Left => Model (New_Item),
408 Right => Model (Container),
409 Fst => Index_Type'First,
410 Lst => Last_Index (New_Item))
412 -- Elements of Container are shifted
415 (Left => Model (Container)'Old,
416 Right => Model (Container),
417 Fst => Index_Type'First,
418 Lst => Last_Index (Container)'Old,
419 Offset => Length (New_Item));
421 procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
423 Pre => Length (Container) < Capacity (Container),
425 Length (Container) = Length (Container)'Old + 1
427 -- Container now has New_Item at Index_Type'First
429 and Element (Model (Container), Index_Type'First) = New_Item
431 -- Elements of Container are shifted by 1
434 (Left => Model (Container)'Old,
435 Right => Model (Container),
436 Fst => Index_Type'First,
437 Lst => Last_Index (Container)'Old,
441 (Container : in out Vector;
442 New_Item : Element_Type;
446 Pre => Length (Container) <= Capacity (Container) - Count,
448 Length (Container) = Length (Container)'Old + Count
450 -- New_Item is inserted Count times at the beginning of Container
453 (Container => Model (Container),
454 Fst => Index_Type'First,
455 Lst => Index_Type'First + Index_Type'Base (Count - 1),
458 -- Elements of Container are shifted
461 (Left => Model (Container)'Old,
462 Right => Model (Container),
463 Fst => Index_Type'First,
464 Lst => Last_Index (Container)'Old,
467 procedure Append (Container : in out Vector; New_Item : Vector) with
470 Length (Container) <= Capacity (Container) - Length (New_Item),
472 Length (Container) = Length (Container)'Old + Length (New_Item)
474 -- The elements of Container are preserved
476 and Model (Container)'Old <= Model (Container)
478 -- Elements of New_Item are inserted at the end of Container
480 and (if Length (New_Item) > 0 then
482 (Left => Model (New_Item),
483 Right => Model (Container),
484 Fst => Index_Type'First,
485 Lst => Last_Index (New_Item),
488 (Last_Index (Container)'Old - Index_Type'First + 1)));
490 procedure Append (Container : in out Vector; New_Item : Element_Type) with
492 Pre => Length (Container) < Capacity (Container),
494 Length (Container) = Length (Container)'Old + 1
496 -- Elements of Container are preserved
498 and Model (Container)'Old < Model (Container)
500 -- Container now has New_Item at the end of Container
503 (Model (Container), Last_Index (Container)'Old + 1) = New_Item;
506 (Container : in out Vector;
507 New_Item : Element_Type;
511 Pre => Length (Container) <= Capacity (Container) - Count,
513 Length (Container) = Length (Container)'Old + Count
515 -- Elements of Container are preserved
517 and Model (Container)'Old <= Model (Container)
519 -- New_Item is inserted Count times at the end of Container
521 and (if Count > 0 then
523 (Container => Model (Container),
524 Fst => Last_Index (Container)'Old + 1,
526 Last_Index (Container)'Old + Index_Type'Base (Count),
529 procedure Delete (Container : in out Vector; Index : Extended_Index) with
531 Pre => Index in First_Index (Container) .. Last_Index (Container),
533 Length (Container) = Length (Container)'Old - 1
535 -- Elements located before Index in Container are preserved
538 (Left => Model (Container)'Old,
539 Right => Model (Container),
540 Fst => Index_Type'First,
543 -- Elements located after Index in Container are shifted by 1
546 (Left => Model (Container),
547 Right => Model (Container)'Old,
549 Lst => Last_Index (Container),
553 (Container : in out Vector;
554 Index : Extended_Index;
559 Index in First_Index (Container) .. Last_Index (Container),
561 Length (Container) in
562 Length (Container)'Old - Count .. Length (Container)'Old
564 -- The elements of Container located before Index are preserved.
567 (Left => Model (Container)'Old,
568 Right => Model (Container),
569 Fst => Index_Type'First,
574 -- All the elements after Position have been erased
576 (Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
577 Length (Container) = Count_Type (Index - Index_Type'First),
580 Length (Container) = Length (Container)'Old - Count
582 -- Other elements are shifted by Count
585 (Left => Model (Container),
586 Right => Model (Container)'Old,
588 Lst => Last_Index (Container),
591 procedure Delete_First (Container : in out Vector) with
593 Pre => Length (Container) > 0,
595 Length (Container) = Length (Container)'Old - 1
597 -- Elements of Container are shifted by 1
600 (Left => Model (Container),
601 Right => Model (Container)'Old,
602 Fst => Index_Type'First,
603 Lst => Last_Index (Container),
606 procedure Delete_First (Container : in out Vector; Count : Count_Type) with
610 -- All the elements of Container have been erased
612 (Length (Container) <= Count => Length (Container) = 0,
615 Length (Container) = Length (Container)'Old - Count
617 -- Elements of Container are shifted by Count
620 (Left => Model (Container),
621 Right => Model (Container)'Old,
622 Fst => Index_Type'First,
623 Lst => Last_Index (Container),
626 procedure Delete_Last (Container : in out Vector) with
628 Pre => Length (Container) > 0,
630 Length (Container) = Length (Container)'Old - 1
632 -- Elements of Container are preserved
634 and Model (Container) < Model (Container)'Old;
636 procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
640 -- All the elements after Position have been erased
642 (Length (Container) <= Count => Length (Container) = 0,
645 Length (Container) = Length (Container)'Old - Count
647 -- The elements of Container are preserved
649 and Model (Container) <= Model (Container)'Old);
651 procedure Reverse_Elements (Container : in out Vector) with
653 Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
656 (Container : in out Vector;
662 I in First_Index (Container) .. Last_Index (Container)
663 and then J in First_Index (Container) .. Last_Index (Container),
665 M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
667 function First_Index (Container : Vector) return Index_Type with
669 Post => First_Index'Result = Index_Type'First;
670 pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
672 function First_Element (Container : Vector) return Element_Type with
674 Pre => not Is_Empty (Container),
676 First_Element'Result = Element (Model (Container), Index_Type'First);
677 pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
679 function Last_Index (Container : Vector) return Extended_Index with
681 Post => Last_Index'Result = M.Last (Model (Container));
682 pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
684 function Last_Element (Container : Vector) return Element_Type with
686 Pre => not Is_Empty (Container),
688 Last_Element'Result =
689 Element (Model (Container), Last_Index (Container));
690 pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
695 Index : Index_Type := Index_Type'First) return Extended_Index
700 -- If Item is not contained in Container after Index, Find_Index
703 (Index > Last_Index (Container)
704 or else not M.Contains
705 (Container => Model (Container),
707 Lst => Last_Index (Container),
710 Find_Index'Result = No_Index,
712 -- Otherwise, Find_Index returns a valid index greater than Index
715 Find_Index'Result in Index .. Last_Index (Container)
717 -- The element at this index in Container is Item
719 and Element (Model (Container), Find_Index'Result) = Item
721 -- It is the first occurrence of Item after Index in Container
724 (Container => Model (Container),
726 Lst => Find_Index'Result - 1,
729 function Reverse_Find_Index
732 Index : Index_Type := Index_Type'Last) return Extended_Index
737 -- If Item is not contained in Container before Index,
738 -- Reverse_Find_Index returns No_Index.
741 (Container => Model (Container),
742 Fst => Index_Type'First,
743 Lst => (if Index <= Last_Index (Container) then Index
744 else Last_Index (Container)),
747 Reverse_Find_Index'Result = No_Index,
749 -- Otherwise, Reverse_Find_Index returns a valid index smaller than
753 Reverse_Find_Index'Result in Index_Type'First .. Index
754 and Reverse_Find_Index'Result <= Last_Index (Container)
756 -- The element at this index in Container is Item
758 and Element (Model (Container), Reverse_Find_Index'Result) = Item
760 -- It is the last occurrence of Item before Index in Container
763 (Container => Model (Container),
764 Fst => Reverse_Find_Index'Result + 1,
766 (if Index <= Last_Index (Container) then
769 Last_Index (Container)),
774 Item : Element_Type) return Boolean
780 (Container => Model (Container),
781 Fst => Index_Type'First,
782 Lst => Last_Index (Container),
787 Position : Extended_Index) return Boolean
792 (Position in Index_Type'First .. Last_Index (Container));
793 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
796 with function "<" (Left, Right : Element_Type) return Boolean is <>;
797 package Generic_Sorting with SPARK_Mode is
799 package Formal_Model with Ghost is
801 function M_Elements_Sorted (Container : M.Sequence) return Boolean
805 M_Elements_Sorted'Result =
806 (for all I in Index_Type'First .. M.Last (Container) =>
807 (for all J in I .. M.Last (Container) =>
808 Element (Container, I) = Element (Container, J)
809 or Element (Container, I) < Element (Container, J)));
810 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
815 function Is_Sorted (Container : Vector) return Boolean with
817 Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
819 procedure Sort (Container : in out Vector) with
822 Length (Container) = Length (Container)'Old
823 and M_Elements_Sorted (Model (Container))
824 and M_Elements_Included
825 (Left => Model (Container)'Old,
826 L_Lst => Last_Index (Container),
827 Right => Model (Container),
828 R_Lst => Last_Index (Container))
829 and M_Elements_Included
830 (Left => Model (Container),
831 L_Lst => Last_Index (Container),
832 Right => Model (Container)'Old,
833 R_Lst => Last_Index (Container));
835 procedure Merge (Target : in out Vector; Source : in out Vector) with
836 -- Target and Source should not be aliased
838 Pre => Length (Source) <= Capacity (Target) - Length (Target),
840 Length (Target) = Length (Target)'Old + Length (Source)'Old
841 and Length (Source) = 0
842 and (if M_Elements_Sorted (Model (Target)'Old)
843 and M_Elements_Sorted (Model (Source)'Old)
845 M_Elements_Sorted (Model (Target)))
846 and M_Elements_Included
847 (Left => Model (Target)'Old,
848 L_Lst => Last_Index (Target)'Old,
849 Right => Model (Target),
850 R_Lst => Last_Index (Target))
851 and M_Elements_Included
852 (Left => Model (Source)'Old,
853 L_Lst => Last_Index (Source)'Old,
854 Right => Model (Target),
855 R_Lst => Last_Index (Target))
856 and M_Elements_In_Union
863 pragma SPARK_Mode (Off);
865 pragma Inline (First_Index);
866 pragma Inline (Last_Index);
867 pragma Inline (Element);
868 pragma Inline (First_Element);
869 pragma Inline (Last_Element);
870 pragma Inline (Replace_Element);
871 pragma Inline (Contains);
873 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
874 type Elements_Array is array (Array_Index range <>) of Element_Type;
875 function "=" (L, R : Elements_Array) return Boolean is abstract;
877 type Vector (Capacity : Capacity_Range) is record
878 Last : Extended_Index := No_Index;
879 Elements : Elements_Array (1 .. Capacity);
882 function Empty_Vector return Vector is
883 ((Capacity => 0, others => <>));
885 end Ada.Containers.Formal_Vectors;