| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT LIBRARY COMPONENTS -- |
| -- -- |
| -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 2014-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- This specification is derived from the Ada Reference Manual for use with -- |
| -- GNAT. The copyright notice above, and the license provisions that follow -- |
| -- apply solely to the contents of the part following the private keyword. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| ------------------------------------------------------------------------------ |
| |
| -- Similar to Ada.Containers.Formal_Vectors. The main difference is that |
| -- Element_Type may be indefinite (but not an unconstrained array). |
| |
| with Ada.Containers.Bounded_Holders; |
| with Ada.Containers.Functional_Vectors; |
| |
| generic |
| type Index_Type is range <>; |
| type Element_Type (<>) is private; |
| with function "=" (Left, Right : Element_Type) return Boolean is <>; |
| Max_Size_In_Storage_Elements : Natural; |
| -- Maximum size of Vector elements in bytes. This has the same meaning as |
| -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that |
| -- setting this too small can lead to erroneous execution; see comments in |
| -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the |
| -- responsibility of clients to calculate the maximum size of all types in |
| -- the class. |
| |
| Bounded : Boolean := True; |
| -- If True, the containers are bounded; the initial capacity is the maximum |
| -- size, and heap allocation will be avoided. If False, the containers can |
| -- grow via heap allocation. |
| |
| package Ada.Containers.Formal_Indefinite_Vectors with |
| SPARK_Mode => On |
| is |
| -- Contracts in this unit are meant for analysis only, not for run-time |
| -- checking. |
| |
| pragma Assertion_Policy (Pre => Ignore); |
| pragma Assertion_Policy (Post => Ignore); |
| pragma Assertion_Policy (Contract_Cases => Ignore); |
| pragma Annotate (CodePeer, Skip_Analysis); |
| |
| subtype Extended_Index is Index_Type'Base |
| range Index_Type'First - 1 .. |
| Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; |
| |
| No_Index : constant Extended_Index := Extended_Index'First; |
| |
| Last_Count : constant Count_Type := |
| (if Index_Type'Last < Index_Type'First then |
| 0 |
| elsif Index_Type'Last < -1 |
| or else Index_Type'Pos (Index_Type'First) > |
| Index_Type'Pos (Index_Type'Last) - Count_Type'Last |
| then |
| Index_Type'Pos (Index_Type'Last) - |
| Index_Type'Pos (Index_Type'First) + 1 |
| else |
| Count_Type'Last); |
| -- Maximal capacity of any vector. It is the minimum of the size of the |
| -- index range and the last possible Count_Type. |
| |
| subtype Capacity_Range is Count_Type range 0 .. Last_Count; |
| |
| type Vector (Capacity : Capacity_Range) is limited private with |
| Default_Initial_Condition => Is_Empty (Vector); |
| -- In the bounded case, Capacity is the capacity of the container, which |
| -- never changes. In the unbounded case, Capacity is the initial capacity |
| -- of the container, and operations such as Reserve_Capacity and Append can |
| -- increase the capacity. The capacity never shrinks, except in the case of |
| -- Clear. |
| -- |
| -- Note that all objects of type Vector are constrained, including in the |
| -- unbounded case; you can't assign from one object to another if the |
| -- Capacity is different. |
| |
| function Length (Container : Vector) return Capacity_Range with |
| Global => null, |
| Post => Length'Result <= Capacity (Container); |
| |
| pragma Unevaluated_Use_Of_Old (Allow); |
| |
| package Formal_Model with Ghost is |
| |
| package M is new Ada.Containers.Functional_Vectors |
| (Index_Type => Index_Type, |
| Element_Type => Element_Type); |
| |
| function "=" |
| (Left : M.Sequence; |
| Right : M.Sequence) return Boolean renames M."="; |
| |
| function "<" |
| (Left : M.Sequence; |
| Right : M.Sequence) return Boolean renames M."<"; |
| |
| function "<=" |
| (Left : M.Sequence; |
| Right : M.Sequence) return Boolean renames M."<="; |
| |
| function M_Elements_In_Union |
| (Container : M.Sequence; |
| Left : M.Sequence; |
| Right : M.Sequence) return Boolean |
| -- The elements of Container are contained in either Left or Right |
| with |
| Global => null, |
| Post => |
| M_Elements_In_Union'Result = |
| (for all I in Index_Type'First .. M.Last (Container) => |
| (for some J in Index_Type'First .. M.Last (Left) => |
| Element (Container, I) = Element (Left, J)) |
| or (for some J in Index_Type'First .. M.Last (Right) => |
| Element (Container, I) = Element (Right, J))); |
| pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); |
| |
| function M_Elements_Included |
| (Left : M.Sequence; |
| L_Fst : Index_Type := Index_Type'First; |
| L_Lst : Extended_Index; |
| Right : M.Sequence; |
| R_Fst : Index_Type := Index_Type'First; |
| R_Lst : Extended_Index) return Boolean |
| -- The elements of the slice from L_Fst to L_Lst in Left are contained |
| -- in the slide from R_Fst to R_Lst in Right. |
| with |
| Global => null, |
| Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right), |
| Post => |
| M_Elements_Included'Result = |
| (for all I in L_Fst .. L_Lst => |
| (for some J in R_Fst .. R_Lst => |
| Element (Left, I) = Element (Right, J))); |
| pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); |
| |
| function M_Elements_Reversed |
| (Left : M.Sequence; |
| Right : M.Sequence) return Boolean |
| -- Right is Left in reverse order |
| with |
| Global => null, |
| Post => |
| M_Elements_Reversed'Result = |
| (M.Length (Left) = M.Length (Right) |
| and (for all I in Index_Type'First .. M.Last (Left) => |
| Element (Left, I) = |
| Element (Right, M.Last (Left) - I + 1)) |
| and (for all I in Index_Type'First .. M.Last (Right) => |
| Element (Right, I) = |
| Element (Left, M.Last (Left) - I + 1))); |
| pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); |
| |
| function M_Elements_Swapped |
| (Left : M.Sequence; |
| Right : M.Sequence; |
| X : Index_Type; |
| Y : Index_Type) return Boolean |
| -- Elements stored at X and Y are reversed in Left and Right |
| with |
| Global => null, |
| Pre => X <= M.Last (Left) and Y <= M.Last (Left), |
| Post => |
| M_Elements_Swapped'Result = |
| (M.Length (Left) = M.Length (Right) |
| and Element (Left, X) = Element (Right, Y) |
| and Element (Left, Y) = Element (Right, X) |
| and M.Equal_Except (Left, Right, X, Y)); |
| pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); |
| |
| function Model (Container : Vector) return M.Sequence with |
| -- The high-level model of a vector is a sequence of elements. The |
| -- sequence really is similar to the vector itself. However, it is not |
| -- limited which allows usage of 'Old and 'Loop_Entry attributes. |
| |
| Ghost, |
| Global => null, |
| Post => M.Length (Model'Result) = Length (Container); |
| |
| function Element |
| (S : M.Sequence; |
| I : Index_Type) return Element_Type renames M.Get; |
| -- To improve readability of contracts, we rename the function used to |
| -- access an element in the model to Element. |
| |
| end Formal_Model; |
| use Formal_Model; |
| |
| function Empty_Vector return Vector with |
| Global => null, |
| Post => Length (Empty_Vector'Result) = 0; |
| |
| function "=" (Left, Right : Vector) return Boolean with |
| Global => null, |
| Post => "="'Result = (Model (Left) = Model (Right)); |
| |
| function To_Vector |
| (New_Item : Element_Type; |
| Length : Capacity_Range) return Vector |
| with |
| Global => null, |
| Post => |
| Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length |
| and M.Constant_Range |
| (Container => Model (To_Vector'Result), |
| Fst => Index_Type'First, |
| Lst => Last_Index (To_Vector'Result), |
| Item => New_Item); |
| |
| function Capacity (Container : Vector) return Capacity_Range with |
| Global => null, |
| Post => |
| Capacity'Result = |
| (if Bounded then |
| Container.Capacity |
| else |
| Capacity_Range'Last); |
| pragma Annotate (GNATprove, Inline_For_Proof, Capacity); |
| |
| procedure Reserve_Capacity |
| (Container : in out Vector; |
| Capacity : Capacity_Range) |
| with |
| Global => null, |
| Pre => (if Bounded then Capacity <= Container.Capacity), |
| Post => Model (Container) = Model (Container)'Old; |
| |
| function Is_Empty (Container : Vector) return Boolean with |
| Global => null, |
| Post => Is_Empty'Result = (Length (Container) = 0); |
| |
| procedure Clear (Container : in out Vector) with |
| Global => null, |
| Post => Length (Container) = 0; |
| -- Note that this reclaims storage in the unbounded case. You need to call |
| -- this before a container goes out of scope in order to avoid storage |
| -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. |
| |
| procedure Assign (Target : in out Vector; Source : Vector) with |
| Global => null, |
| Pre => (if Bounded then Length (Source) <= Target.Capacity), |
| Post => Model (Target) = Model (Source); |
| |
| function Copy |
| (Source : Vector; |
| Capacity : Capacity_Range := 0) return Vector |
| with |
| Global => null, |
| Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), |
| Post => |
| Model (Copy'Result) = Model (Source) |
| and (if Capacity = 0 then |
| Copy'Result.Capacity = Length (Source) |
| else |
| Copy'Result.Capacity = Capacity); |
| |
| procedure Move (Target : in out Vector; Source : in out Vector) |
| with |
| Global => null, |
| Pre => (if Bounded then Length (Source) <= Capacity (Target)), |
| Post => Model (Target) = Model (Source)'Old and Length (Source) = 0; |
| |
| function Element |
| (Container : Vector; |
| Index : Index_Type) return Element_Type |
| with |
| Global => null, |
| Pre => Index in First_Index (Container) .. Last_Index (Container), |
| Post => Element'Result = Element (Model (Container), Index); |
| pragma Annotate (GNATprove, Inline_For_Proof, Element); |
| |
| procedure Replace_Element |
| (Container : in out Vector; |
| Index : Index_Type; |
| New_Item : Element_Type) |
| with |
| Global => null, |
| Pre => Index in First_Index (Container) .. Last_Index (Container), |
| Post => |
| Length (Container) = Length (Container)'Old |
| |
| -- Container now has New_Item at index Index |
| |
| and Element (Model (Container), Index) = New_Item |
| |
| -- All other elements are preserved |
| |
| and M.Equal_Except |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Position => Index); |
| |
| function At_End (E : access constant Vector) return access constant Vector |
| is (E) |
| with Ghost, |
| Annotate => (GNATprove, At_End_Borrow); |
| |
| function At_End |
| (E : access constant Element_Type) return access constant Element_Type |
| is (E) |
| with Ghost, |
| Annotate => (GNATprove, At_End_Borrow); |
| |
| function Constant_Reference |
| (Container : aliased Vector; |
| Index : Index_Type) return not null access constant Element_Type |
| with |
| Global => null, |
| Pre => Index in First_Index (Container) .. Last_Index (Container), |
| Post => |
| Constant_Reference'Result.all = Element (Model (Container), Index); |
| |
| function Reference |
| (Container : not null access Vector; |
| Index : Index_Type) return not null access Element_Type |
| with |
| Global => null, |
| Pre => |
| Index in First_Index (Container.all) .. Last_Index (Container.all), |
| Post => |
| Length (Container.all) = Length (At_End (Container).all) |
| |
| -- Container will have Result.all at index Index |
| |
| and At_End (Reference'Result).all = |
| Element (Model (At_End (Container).all), Index) |
| |
| -- All other elements are preserved |
| |
| and M.Equal_Except |
| (Left => Model (Container.all), |
| Right => Model (At_End (Container).all), |
| Position => Index); |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Vector) |
| with |
| Global => null, |
| Pre => |
| Length (Container) <= Capacity (Container) - Length (New_Item) |
| and (Before in Index_Type'First .. Last_Index (Container) |
| or (Before /= No_Index |
| and then Before - 1 = Last_Index (Container))), |
| Post => |
| Length (Container) = Length (Container)'Old + Length (New_Item) |
| |
| -- Elements located before Before in Container are preserved |
| |
| and M.Range_Equal |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Before - 1) |
| |
| -- Elements of New_Item are inserted at position Before |
| |
| and (if Length (New_Item) > 0 then |
| M.Range_Shifted |
| (Left => Model (New_Item), |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (New_Item), |
| Offset => Count_Type (Before - Index_Type'First))) |
| |
| -- Elements located after Before in Container are shifted |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Before, |
| Lst => Last_Index (Container)'Old, |
| Offset => Length (New_Item)); |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Element_Type) |
| with |
| Global => null, |
| Pre => |
| Length (Container) < Capacity (Container) |
| and then (Before in Index_Type'First .. Last_Index (Container) + 1), |
| Post => |
| Length (Container) = Length (Container)'Old + 1 |
| |
| -- Elements located before Before in Container are preserved |
| |
| and M.Range_Equal |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Before - 1) |
| |
| -- Container now has New_Item at index Before |
| |
| and Element (Model (Container), Before) = New_Item |
| |
| -- Elements located after Before in Container are shifted by 1 |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Before, |
| Lst => Last_Index (Container)'Old, |
| Offset => 1); |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| with |
| Global => null, |
| Pre => |
| Length (Container) <= Capacity (Container) - Count |
| and (Before in Index_Type'First .. Last_Index (Container) |
| or (Before /= No_Index |
| and then Before - 1 = Last_Index (Container))), |
| Post => |
| Length (Container) = Length (Container)'Old + Count |
| |
| -- Elements located before Before in Container are preserved |
| |
| and M.Range_Equal |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Before - 1) |
| |
| -- New_Item is inserted Count times at position Before |
| |
| and (if Count > 0 then |
| M.Constant_Range |
| (Container => Model (Container), |
| Fst => Before, |
| Lst => Before + Index_Type'Base (Count - 1), |
| Item => New_Item)) |
| |
| -- Elements located after Before in Container are shifted |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Before, |
| Lst => Last_Index (Container)'Old, |
| Offset => Count); |
| |
| procedure Prepend (Container : in out Vector; New_Item : Vector) with |
| Global => null, |
| Pre => Length (Container) <= Capacity (Container) - Length (New_Item), |
| Post => |
| Length (Container) = Length (Container)'Old + Length (New_Item) |
| |
| -- Elements of New_Item are inserted at the beginning of Container |
| |
| and M.Range_Equal |
| (Left => Model (New_Item), |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (New_Item)) |
| |
| -- Elements of Container are shifted |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container)'Old, |
| Offset => Length (New_Item)); |
| |
| procedure Prepend (Container : in out Vector; New_Item : Element_Type) with |
| Global => null, |
| Pre => Length (Container) < Capacity (Container), |
| Post => |
| Length (Container) = Length (Container)'Old + 1 |
| |
| -- Container now has New_Item at Index_Type'First |
| |
| and Element (Model (Container), Index_Type'First) = New_Item |
| |
| -- Elements of Container are shifted by 1 |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container)'Old, |
| Offset => 1); |
| |
| procedure Prepend |
| (Container : in out Vector; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| with |
| Global => null, |
| Pre => Length (Container) <= Capacity (Container) - Count, |
| Post => |
| Length (Container) = Length (Container)'Old + Count |
| |
| -- New_Item is inserted Count times at the beginning of Container |
| |
| and M.Constant_Range |
| (Container => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Index_Type'First + Index_Type'Base (Count - 1), |
| Item => New_Item) |
| |
| -- Elements of Container are shifted |
| |
| and M.Range_Shifted |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container)'Old, |
| Offset => Count); |
| |
| procedure Append (Container : in out Vector; New_Item : Vector) with |
| Global => null, |
| Pre => |
| Length (Container) <= Capacity (Container) - Length (New_Item), |
| Post => |
| Length (Container) = Length (Container)'Old + Length (New_Item) |
| |
| -- The elements of Container are preserved |
| |
| and Model (Container)'Old <= Model (Container) |
| |
| -- Elements of New_Item are inserted at the end of Container |
| |
| and (if Length (New_Item) > 0 then |
| M.Range_Shifted |
| (Left => Model (New_Item), |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (New_Item), |
| Offset => |
| Count_Type |
| (Last_Index (Container)'Old - Index_Type'First + 1))); |
| |
| procedure Append (Container : in out Vector; New_Item : Element_Type) with |
| Global => null, |
| Pre => Length (Container) < Capacity (Container), |
| Post => |
| Length (Container) = Length (Container)'Old + 1 |
| |
| -- Elements of Container are preserved |
| |
| and Model (Container)'Old < Model (Container) |
| |
| -- Container now has New_Item at the end of Container |
| |
| and Element |
| (Model (Container), Last_Index (Container)'Old + 1) = New_Item; |
| |
| procedure Append |
| (Container : in out Vector; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| with |
| Global => null, |
| Pre => Length (Container) <= Capacity (Container) - Count, |
| Post => |
| Length (Container) = Length (Container)'Old + Count |
| |
| -- Elements of Container are preserved |
| |
| and Model (Container)'Old <= Model (Container) |
| |
| -- New_Item is inserted Count times at the end of Container |
| |
| and (if Count > 0 then |
| M.Constant_Range |
| (Container => Model (Container), |
| Fst => Last_Index (Container)'Old + 1, |
| Lst => |
| Last_Index (Container)'Old + Index_Type'Base (Count), |
| Item => New_Item)); |
| |
| procedure Delete (Container : in out Vector; Index : Extended_Index) with |
| Global => null, |
| Pre => Index in First_Index (Container) .. Last_Index (Container), |
| Post => |
| Length (Container) = Length (Container)'Old - 1 |
| |
| -- Elements located before Index in Container are preserved |
| |
| and M.Range_Equal |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Index - 1) |
| |
| -- Elements located after Index in Container are shifted by 1 |
| |
| and M.Range_Shifted |
| (Left => Model (Container), |
| Right => Model (Container)'Old, |
| Fst => Index, |
| Lst => Last_Index (Container), |
| Offset => 1); |
| |
| procedure Delete |
| (Container : in out Vector; |
| Index : Extended_Index; |
| Count : Count_Type) |
| with |
| Global => null, |
| Pre => |
| Index in First_Index (Container) .. Last_Index (Container), |
| Post => |
| Length (Container) in |
| Length (Container)'Old - Count .. Length (Container)'Old |
| |
| -- The elements of Container located before Index are preserved. |
| |
| and M.Range_Equal |
| (Left => Model (Container)'Old, |
| Right => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Index - 1), |
| |
| Contract_Cases => |
| |
| -- All the elements after Position have been erased |
| |
| (Length (Container) - Count <= Count_Type (Index - Index_Type'First) => |
| Length (Container) = Count_Type (Index - Index_Type'First), |
| |
| others => |
| Length (Container) = Length (Container)'Old - Count |
| |
| -- Other elements are shifted by Count |
| |
| and M.Range_Shifted |
| (Left => Model (Container), |
| Right => Model (Container)'Old, |
| Fst => Index, |
| Lst => Last_Index (Container), |
| Offset => Count)); |
| |
| procedure Delete_First (Container : in out Vector) with |
| Global => null, |
| Pre => Length (Container) > 0, |
| Post => |
| Length (Container) = Length (Container)'Old - 1 |
| |
| -- Elements of Container are shifted by 1 |
| |
| and M.Range_Shifted |
| (Left => Model (Container), |
| Right => Model (Container)'Old, |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container), |
| Offset => 1); |
| |
| procedure Delete_First (Container : in out Vector; Count : Count_Type) with |
| Global => null, |
| Contract_Cases => |
| |
| -- All the elements of Container have been erased |
| |
| (Length (Container) <= Count => Length (Container) = 0, |
| |
| others => |
| Length (Container) = Length (Container)'Old - Count |
| |
| -- Elements of Container are shifted by Count |
| |
| and M.Range_Shifted |
| (Left => Model (Container), |
| Right => Model (Container)'Old, |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container), |
| Offset => Count)); |
| |
| procedure Delete_Last (Container : in out Vector) with |
| Global => null, |
| Pre => Length (Container) > 0, |
| Post => |
| Length (Container) = Length (Container)'Old - 1 |
| |
| -- Elements of Container are preserved |
| |
| and Model (Container) < Model (Container)'Old; |
| |
| procedure Delete_Last (Container : in out Vector; Count : Count_Type) with |
| Global => null, |
| Contract_Cases => |
| |
| -- All the elements after Position have been erased |
| |
| (Length (Container) <= Count => Length (Container) = 0, |
| |
| others => |
| Length (Container) = Length (Container)'Old - Count |
| |
| -- The elements of Container are preserved |
| |
| and Model (Container) <= Model (Container)'Old); |
| |
| procedure Reverse_Elements (Container : in out Vector) with |
| Global => null, |
| Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); |
| |
| procedure Swap |
| (Container : in out Vector; |
| I : Index_Type; |
| J : Index_Type) |
| with |
| Global => null, |
| Pre => |
| I in First_Index (Container) .. Last_Index (Container) |
| and then J in First_Index (Container) .. Last_Index (Container), |
| Post => |
| M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); |
| |
| function First_Index (Container : Vector) return Index_Type with |
| Global => null, |
| Post => First_Index'Result = Index_Type'First; |
| pragma Annotate (GNATprove, Inline_For_Proof, First_Index); |
| |
| function First_Element (Container : Vector) return Element_Type with |
| Global => null, |
| Pre => not Is_Empty (Container), |
| Post => |
| First_Element'Result = Element (Model (Container), Index_Type'First); |
| pragma Annotate (GNATprove, Inline_For_Proof, First_Element); |
| |
| function Last_Index (Container : Vector) return Extended_Index with |
| Global => null, |
| Post => Last_Index'Result = M.Last (Model (Container)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Last_Index); |
| |
| function Last_Element (Container : Vector) return Element_Type with |
| Global => null, |
| Pre => not Is_Empty (Container), |
| Post => |
| Last_Element'Result = |
| Element (Model (Container), Last_Index (Container)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Last_Element); |
| |
| function Find_Index |
| (Container : Vector; |
| Item : Element_Type; |
| Index : Index_Type := Index_Type'First) return Extended_Index |
| with |
| Global => null, |
| Contract_Cases => |
| |
| -- If Item is not contained in Container after Index, Find_Index |
| -- returns No_Index. |
| |
| (Index > Last_Index (Container) |
| or else not M.Contains |
| (Container => Model (Container), |
| Fst => Index, |
| Lst => Last_Index (Container), |
| Item => Item) |
| => |
| Find_Index'Result = No_Index, |
| |
| -- Otherwise, Find_Index returns a valid index greater than Index |
| |
| others => |
| Find_Index'Result in Index .. Last_Index (Container) |
| |
| -- The element at this index in Container is Item |
| |
| and Element (Model (Container), Find_Index'Result) = Item |
| |
| -- It is the first occurrence of Item after Index in Container |
| |
| and not M.Contains |
| (Container => Model (Container), |
| Fst => Index, |
| Lst => Find_Index'Result - 1, |
| Item => Item)); |
| |
| function Reverse_Find_Index |
| (Container : Vector; |
| Item : Element_Type; |
| Index : Index_Type := Index_Type'Last) return Extended_Index |
| with |
| Global => null, |
| Contract_Cases => |
| |
| -- If Item is not contained in Container before Index, |
| -- Reverse_Find_Index returns No_Index. |
| |
| (not M.Contains |
| (Container => Model (Container), |
| Fst => Index_Type'First, |
| Lst => (if Index <= Last_Index (Container) then Index |
| else Last_Index (Container)), |
| Item => Item) |
| => |
| Reverse_Find_Index'Result = No_Index, |
| |
| -- Otherwise, Reverse_Find_Index returns a valid index smaller than |
| -- Index |
| |
| others => |
| Reverse_Find_Index'Result in Index_Type'First .. Index |
| and Reverse_Find_Index'Result <= Last_Index (Container) |
| |
| -- The element at this index in Container is Item |
| |
| and Element (Model (Container), Reverse_Find_Index'Result) = Item |
| |
| -- It is the last occurrence of Item before Index in Container |
| |
| and not M.Contains |
| (Container => Model (Container), |
| Fst => Reverse_Find_Index'Result + 1, |
| Lst => |
| (if Index <= Last_Index (Container) then |
| Index |
| else |
| Last_Index (Container)), |
| Item => Item)); |
| |
| function Contains |
| (Container : Vector; |
| Item : Element_Type) return Boolean |
| with |
| Global => null, |
| Post => |
| Contains'Result = |
| M.Contains |
| (Container => Model (Container), |
| Fst => Index_Type'First, |
| Lst => Last_Index (Container), |
| Item => Item); |
| |
| function Has_Element |
| (Container : Vector; |
| Position : Extended_Index) return Boolean |
| with |
| Global => null, |
| Post => |
| Has_Element'Result = |
| (Position in Index_Type'First .. Last_Index (Container)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); |
| |
| generic |
| with function "<" (Left, Right : Element_Type) return Boolean is <>; |
| package Generic_Sorting with SPARK_Mode is |
| |
| package Formal_Model with Ghost is |
| |
| function M_Elements_Sorted (Container : M.Sequence) return Boolean |
| with |
| Global => null, |
| Post => |
| M_Elements_Sorted'Result = |
| (for all I in Index_Type'First .. M.Last (Container) => |
| (for all J in I .. M.Last (Container) => |
| Element (Container, I) = Element (Container, J) |
| or Element (Container, I) < Element (Container, J))); |
| pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); |
| |
| end Formal_Model; |
| use Formal_Model; |
| |
| function Is_Sorted (Container : Vector) return Boolean with |
| Global => null, |
| Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container)); |
| |
| procedure Sort (Container : in out Vector) with |
| Global => null, |
| Post => |
| Length (Container) = Length (Container)'Old |
| and M_Elements_Sorted (Model (Container)) |
| and M_Elements_Included |
| (Left => Model (Container)'Old, |
| L_Lst => Last_Index (Container), |
| Right => Model (Container), |
| R_Lst => Last_Index (Container)) |
| and M_Elements_Included |
| (Left => Model (Container), |
| L_Lst => Last_Index (Container), |
| Right => Model (Container)'Old, |
| R_Lst => Last_Index (Container)); |
| |
| procedure Merge (Target : in out Vector; Source : in out Vector) with |
| -- Target and Source should not be aliased |
| Global => null, |
| Pre => Length (Source) <= Capacity (Target) - Length (Target), |
| Post => |
| Length (Target) = Length (Target)'Old + Length (Source)'Old |
| and Length (Source) = 0 |
| and (if M_Elements_Sorted (Model (Target)'Old) |
| and M_Elements_Sorted (Model (Source)'Old) |
| then |
| M_Elements_Sorted (Model (Target))) |
| and M_Elements_Included |
| (Left => Model (Target)'Old, |
| L_Lst => Last_Index (Target)'Old, |
| Right => Model (Target), |
| R_Lst => Last_Index (Target)) |
| and M_Elements_Included |
| (Left => Model (Source)'Old, |
| L_Lst => Last_Index (Source)'Old, |
| Right => Model (Target), |
| R_Lst => Last_Index (Target)) |
| and M_Elements_In_Union |
| (Model (Target), |
| Model (Source)'Old, |
| Model (Target)'Old); |
| end Generic_Sorting; |
| |
| private |
| pragma SPARK_Mode (Off); |
| |
| pragma Inline (First_Index); |
| pragma Inline (Last_Index); |
| pragma Inline (Element); |
| pragma Inline (First_Element); |
| pragma Inline (Last_Element); |
| pragma Inline (Replace_Element); |
| pragma Inline (Contains); |
| |
| -- The implementation method is to instantiate Bounded_Holders to get a |
| -- definite type for Element_Type. |
| |
| package Holders is new Bounded_Holders |
| (Element_Type, Max_Size_In_Storage_Elements, "="); |
| use Holders; |
| |
| subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; |
| type Elements_Array is array (Array_Index range <>) of aliased Holder; |
| function "=" (L, R : Elements_Array) return Boolean is abstract; |
| |
| type Elements_Array_Ptr is access all Elements_Array; |
| |
| type Vector (Capacity : Capacity_Range) is limited record |
| |
| -- In the bounded case, the elements are stored in Elements. In the |
| -- unbounded case, the elements are initially stored in Elements, until |
| -- we run out of room, then we switch to Elements_Ptr. |
| |
| Last : Extended_Index := No_Index; |
| Elements_Ptr : Elements_Array_Ptr := null; |
| Elements : aliased Elements_Array (1 .. Capacity); |
| end record; |
| |
| -- The primary reason Vector is limited is that in the unbounded case, once |
| -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will |
| -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, |
| -- so for example "Append (X, ...);" will modify BOTH X and Y. That would |
| -- allow SPARK to "prove" things that are false. We could fix that by |
| -- making Vector a controlled type, and override Adjust to make a deep |
| -- copy, but finalization is not allowed in SPARK. |
| -- |
| -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not |
| -- allowed on Vectors. |
| |
| function Empty_Vector return Vector is |
| ((Capacity => 0, others => <>)); |
| |
| end Ada.Containers.Formal_Indefinite_Vectors; |
