From 394fa9f54a4fc7f2cc6ea0630f948f0e47558e28 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Thu, 27 Apr 2017 09:10:44 +0000 Subject: [PATCH] a-cofuba.ads (Add): Take as an additional input parameter the position where the element should be... 2017-04-27 Claire Dross * a-cofuba.ads (Add): Take as an additional input parameter the position where the element should be inserted. (Remove): New function that removes an element from the container. * a-cofuma.ads (Add): Adapt to the new API of Base.Add. * a-cofuse.ads (Add): Adapt to the new API of Base.Add. (Remove): New function that removes an element from a set. * a-cofuve.ads (Add): Adapt to the new API of Base.Add. (Remove): New function that removes an element from a sequence. (Insert): New function that adds anywhere in a sequence. From-SVN: r247297 --- gcc/ada/ChangeLog | 12 +++++++ gcc/ada/a-cofuba.adb | 58 ++++++++++++++++++++++++--------- gcc/ada/a-cofuba.ads | 34 ++++++++++++------- gcc/ada/a-cofuma.adb | 7 ++-- gcc/ada/a-cofuma.ads | 29 +++++++++-------- gcc/ada/a-cofuse.adb | 52 ++++++++++++++++-------------- gcc/ada/a-cofuse.ads | 37 ++++++++++++++------- gcc/ada/a-cofuve.adb | 26 ++++++++++++--- gcc/ada/a-cofuve.ads | 77 ++++++++++++++++++++++++++++++++------------ 9 files changed, 227 insertions(+), 105 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 91c78f8371f..f6bf798fe54 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2017-04-27 Claire Dross + + * a-cofuba.ads (Add): Take as an additional input parameter + the position where the element should be inserted. + (Remove): New function that removes an element from the container. + * a-cofuma.ads (Add): Adapt to the new API of Base.Add. + * a-cofuse.ads (Add): Adapt to the new API of Base.Add. + (Remove): New function that removes an element from a set. + * a-cofuve.ads (Add): Adapt to the new API of Base.Add. + (Remove): New function that removes an element from a sequence. + (Insert): New function that adds anywhere in a sequence. + 2017-04-27 Hristian Kirtchev * checks.adb (Generate_Range_Check): Revert previous change. diff --git a/gcc/ada/a-cofuba.adb b/gcc/ada/a-cofuba.adb index dd29eea2f56..63ebc5f205b 100644 --- a/gcc/ada/a-cofuba.adb +++ b/gcc/ada/a-cofuba.adb @@ -33,21 +33,17 @@ pragma Ada_2012; package body Ada.Containers.Functional_Base with SPARK_Mode => Off is - pragma Assertion_Policy - (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); - function To_Count (Idx : Extended_Index) return Count_Type is (Count_Type - (Extended_Index'Pos (Idx) - - Extended_Index'Pos (Extended_Index'First))); + (Extended_Index'Pos (Idx) + - Extended_Index'Pos (Extended_Index'First))); function To_Index (Position : Count_Type) return Extended_Index is (Extended_Index'Val - (Position - + Extended_Index'Pos (Extended_Index'First))); + (Position + Extended_Index'Pos (Extended_Index'First))); -- Conversion functions between Index_Type and Count_Type function Find (C : Container; E : access Element_Type) return Count_Type; - -- Search a container C for an element equal to E.all, return the + -- Search a container C for an element equal to E.all, returning the -- position in the underlying array. --------- @@ -86,11 +82,24 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is -- Add -- --------- - function Add (C : Container; E : Element_Type) return Container is + function Add + (C : Container; + I : Index_Type; + E : Element_Type) return Container + is + A : constant Element_Array_Access := + new Element_Array'(1 .. C.Elements'Last + 1 => <>); + P : Count_Type := 0; begin - return Container'(Elements => - new Element_Array' - (C.Elements.all & new Element_Type'(E))); + for J in 1 .. C.Elements'Last + 1 loop + if J /= To_Count (I) then + P := P + 1; + A (J) := C.Elements (P); + else + A (J) := new Element_Type'(E); + end if; + end loop; + return Container'(Elements => A); end Add; ---------- @@ -123,7 +132,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is function Intersection (C1, C2 : Container) return Container is A : constant Element_Array_Access := - new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>); + new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>); P : Count_Type := 0; begin for I in C1.Elements'Range loop @@ -139,8 +148,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is -- Length -- ------------ - function Length (C : Container) return Count_Type is - (C.Elements'Length); + function Length (C : Container) return Count_Type is (C.Elements'Length); --------------------- -- Num_Overlaps -- @@ -157,6 +165,24 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is return P; end Num_Overlaps; + ------------ + -- Remove -- + ------------ + + function Remove (C : Container; I : Index_Type) return Container is + A : constant Element_Array_Access := + new Element_Array'(1 .. C.Elements'Last - 1 => <>); + P : Count_Type := 0; + begin + for J in C.Elements'Range loop + if J /= To_Count (I) then + P := P + 1; + A (P) := C.Elements (J); + end if; + end loop; + return Container'(Elements => A); + end Remove; + --------- -- Set -- --------- @@ -165,7 +191,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is return Container is Result : constant Container := - Container'(Elements => new Element_Array'(C.Elements.all)); + Container'(Elements => new Element_Array'(C.Elements.all)); begin Result.Elements (To_Count (I)) := new Element_Type'(E); return Result; diff --git a/gcc/ada/a-cofuba.ads b/gcc/ada/a-cofuba.ads index 6bcea9d2022..e1760712d72 100644 --- a/gcc/ada/a-cofuba.ads +++ b/gcc/ada/a-cofuba.ads @@ -28,16 +28,16 @@ -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- -- . -- ------------------------------------------------------------------------------ --- Functional containers are neither controlled nor limited. This is safe as --- no primitives is provided to modify them. +-- Functional containers are neither controlled nor limited. This is safe, as +-- no primitives are provided to modify them. -- Memory allocated inside functional containers is never reclaimed. pragma Ada_2012; private generic type Index_Type is (<>); - -- To avoid Constraint_Error being raised at runtime, Index_Type'Base - -- should have at least one more element at the left than Index_Type. + -- To avoid Constraint_Error being raised at run time, Index_Type'Base + -- should have at least one more element at the low end than Index_Type. type Element_Type (<>) is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; @@ -52,22 +52,28 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is -- Return True if C1 and C2 contain the same elements at the same position function Length (C : Container) return Count_Type; - -- Number of elements stored in C. + -- Number of elements stored in C function Get (C : Container; I : Index_Type) return Element_Type; - -- Access to the element at index I in C. + -- Access to the element at index I in C function Set (C : Container; I : Index_Type; E : Element_Type) return Container; -- Return a new container which is equal to C except for the element at - -- index I which is set to E. + -- index I, which is set to E. - function Add (C : Container; E : Element_Type) return Container; - -- Return a new container which is C appended with E. + function Add + (C : Container; + I : Index_Type; + E : Element_Type) return Container; + -- Return a new container that is C with E inserted at index I + + function Remove (C : Container; I : Index_Type) return Container; + -- Return a new container that is C without the element at index I function Find (C : Container; E : Element_Type) return Extended_Index; - -- Return the first index for which the element stored in C is I. - -- If there are no such indexes, return Extended_Index'First. + -- Return the first index for which the element stored in C is I. If there + -- are no such indexes, return Extended_Index'First. -------------------- -- Set Operations -- @@ -77,7 +83,7 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is -- Return True if every element of C1 is in C2 function Num_Overlaps (C1, C2 : Container) return Count_Type; - -- Return the number of elements that are both in + -- Return the number of elements that are in both C1 and C2 function Union (C1, C2 : Container) return Container; -- Return a container which is C1 plus all the elements of C2 that are not @@ -92,13 +98,17 @@ private subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; type Element_Access is access all Element_Type; + type Element_Array is array (Positive_Count_Type range <>) of Element_Access; + type Element_Array_Access is not null access Element_Array; + Empty_Element_Array_Access : constant Element_Array_Access := new Element_Array'(1 .. 0 => null); type Container is record Elements : Element_Array_Access := Empty_Element_Array_Access; end record; + end Ada.Containers.Functional_Base; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index 9367baeea13..742320c6f89 100644 --- a/gcc/ada/a-cofuma.adb +++ b/gcc/ada/a-cofuma.adb @@ -34,9 +34,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is use Key_Containers; use Element_Containers; - pragma Assertion_Policy - (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); - --------- -- "=" -- --------- @@ -69,8 +66,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is function Add (M : Map; K : Key_Type; E : Element_Type) return Map is begin return - (Keys => Add (M.Keys, K), - Elements => Add (M.Elements, E)); + (Keys => Add (M.Keys, Length (M.Keys) + 1, K), + Elements => Add (M.Elements, Length (M.Elements) + 1, E)); end Add; --------- diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 23fb45c0a9d..960264c21d7 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -39,6 +39,8 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Functional_Maps with SPARK_Mode is + pragma Assertion_Policy (Post => Ignore); + type Map is private with Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0, Iterable => (First => Iter_First, @@ -46,10 +48,10 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Has_Element => Iter_Has_Element, Element => Iter_Element); -- Maps are empty when default initialized. - -- For in quantification over maps should not be used. - -- For of quantification over maps iterates over keys. + -- "For in" quantification over maps should not be used. + -- "For of" quantification over maps iterates over keys. - -- Maps are axiomatized using Mem and Get encoding respectively the + -- Maps are axiomatized using Mem and Get, encoding respectively the -- presence of a key in a map and an accessor to elements associated to its -- keys. The length of a map is also added to protect Add against overflows -- but it is not actually modeled. @@ -64,7 +66,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Global => null; function "<=" (M1, M2 : Map) return Boolean with - -- Map inclusion. + -- Map inclusion Global => null, Post => "<="'Result = @@ -72,25 +74,23 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is and then Get (M2, K) = Get (M1, K)); function "=" (M1, M2 : Map) return Boolean with - -- Extensional equality over maps. + -- Extensional equality over maps Global => null, Post => "="'Result = - ((for all K of M1 => Mem (M2, K) - and then Get (M2, K) = Get (M1, K)) - and (for all K of M2 => Mem (M1, K))); + ((for all K of M1 => Mem (M2, K) and then Get (M2, K) = Get (M1, K)) + and (for all K of M2 => Mem (M1, K))); pragma Warnings (Off, "unused variable ""K"""); function Is_Empty (M : Map) return Boolean with - -- A map is empty if it contains no key. - + -- A map is empty if it contains no key Global => null, Post => Is_Empty'Result = (for all K of M => False); pragma Warnings (On, "unused variable ""K"""); function Is_Add (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean - -- Returns True if Result is M augmented with the mapping K -> E. + -- Returns True if Result is M augmented with the mapping K -> E with Global => null, @@ -115,7 +115,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is function Is_Set (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean - -- Returns True if Result is M where the element associated to K has been + -- Returns True if Result is M, where the element associated to K has been -- replaced by E. with @@ -130,7 +130,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is and then (for all K of Result => Mem (M, K))); function Set (M : Map; K : Key_Type; E : Element_Type) return Map with - -- Returns M where the element associated to K has been replaced by E. + -- Returns M, where the element associated to K has been replaced by E. -- Is_Set (M, K, E, Result) should be used instead of -- Result = Set (M, K, E) whenever possible both for execution and for -- proof. @@ -157,7 +157,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Global => null, Pre => Iter_Has_Element (M, K); pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem); + private + pragma SPARK_Mode (Off); function "=" (Left, Right : Key_Type) return Boolean @@ -190,4 +192,5 @@ private function Iter_Element (M : Map; K : Private_Key) return Key_Type is (Key_Containers.Get (M.Keys, Count_Type (K))); + end Ada.Containers.Functional_Maps; diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb index 21417b2eda7..8a3d08d9a2f 100644 --- a/gcc/ada/a-cofuse.adb +++ b/gcc/ada/a-cofuse.adb @@ -34,9 +34,6 @@ pragma Ada_2012; package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is use Containers; - pragma Assertion_Policy - (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); - --------- -- "=" -- --------- @@ -55,27 +52,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is --------- function Add (S : Set; E : Element_Type) return Set is - (Content => Add (S.Content, E)); - - ------------ - -- Length -- - ------------ - - function Length (S : Set) return Count_Type is (Length (S.Content)); - - --------- - -- Mem -- - --------- - - function Mem (S : Set; E : Element_Type) return Boolean is - (Find (S.Content, E) > 0); - - ------------------ - -- Num_Overlaps -- - ------------------ - - function Num_Overlaps (S1, S2 : Set) return Count_Type is - (Num_Overlaps (S1.Content, S2.Content)); + (Content => Add (S.Content, Length (S.Content) + 1, E)); ------------------ -- Intersection -- @@ -119,6 +96,33 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is and (for all E of S1 => Mem (Result, E)) and (for all E of S2 => Mem (Result, E))); + ------------ + -- Length -- + ------------ + + function Length (S : Set) return Count_Type is (Length (S.Content)); + + --------- + -- Mem -- + --------- + + function Mem (S : Set; E : Element_Type) return Boolean is + (Find (S.Content, E) > 0); + + ------------------ + -- Num_Overlaps -- + ------------------ + + function Num_Overlaps (S1, S2 : Set) return Count_Type is + (Num_Overlaps (S1.Content, S2.Content)); + + ------------ + -- Remove -- + ------------ + + function Remove (S : Set; E : Element_Type) return Set is + (Content => Remove (S.Content, Find (S.Content, E))); + ----------- -- Union -- ----------- diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index cbc03fa8e04..6f4dc98ad4d 100644 --- a/gcc/ada/a-cofuse.ads +++ b/gcc/ada/a-cofuse.ads @@ -37,6 +37,8 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Functional_Sets with SPARK_Mode is + pragma Assertion_Policy (Post => Ignore); + type Set is private with Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0, Iterable => (First => Iter_First, @@ -44,11 +46,11 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Has_Element => Iter_Has_Element, Element => Iter_Element); -- Sets are empty when default initialized. - -- For in quantification over sets should not be used. - -- For of quantification over sets iterates over elements. + -- "For in" quantification over sets should not be used. + -- "For of" quantification over sets iterates over elements. - -- Sets are axiomatized using Mem which encodes whether an element is - -- contained in a set. The length of a set is also added to protect Add + -- Sets are axiomatized using Mem, which encodes whether an element is + -- contained in a set. The length of a set is also added to protect Add -- against overflows but it is not actually modeled. function Mem (S : Set; E : Element_Type) return Boolean with @@ -58,13 +60,13 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Global => null; function "<=" (S1, S2 : Set) return Boolean with - -- Set inclusion. + -- Set inclusion Global => null, Post => "<="'Result = (for all E of S1 => Mem (S2, E)); function "=" (S1, S2 : Set) return Boolean with - -- Extensional equality over sets. + -- Extensional equality over sets Global => null, Post => @@ -73,14 +75,14 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is pragma Warnings (Off, "unused variable ""E"""); function Is_Empty (S : Set) return Boolean with - -- A set is empty if it contains no element. + -- A set is empty if it contains no element Global => null, Post => Is_Empty'Result = (for all E of S => False); pragma Warnings (On, "unused variable ""E"""); function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean - -- Returns True if Result is S augmented with E. + -- Returns True if Result is S augmented with E with Global => null, @@ -99,8 +101,18 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Post => Length (Add'Result) = Length (S) + 1 and Is_Add (S, E, Add'Result); + function Remove (S : Set; E : Element_Type) return Set with + -- Returns S without E. + -- Is_Add (Result, E, S) should be used instead of Result = Remove (S, E) + -- whenever possible both for execution and for proof. + + Global => null, + Pre => Mem (S, E), + Post => Length (Remove'Result) = Length (S) - 1 + and Is_Add (Remove'Result, E, S); + function Is_Intersection (S1, S2, Result : Set) return Boolean with - -- Returns True if Result is the intersection of S1 and S2. + -- Returns True if Result is the intersection of S1 and S2 Global => null, Post => Is_Intersection'Result = @@ -110,7 +122,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is (if Mem (S2, E) then Mem (Result, E)))); function Num_Overlaps (S1, S2 : Set) return Count_Type with - -- Number of elements that are both in S1 and S2. + -- Number of elements that are both in S1 and S2 Global => null, Post => Num_Overlaps'Result <= Length (S1) @@ -129,7 +141,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is and Is_Intersection (S1, S2, Intersection'Result); function Is_Union (S1, S2, Result : Set) return Boolean with - -- Returns True if Result is the union of S1 and S2. + -- Returns True if Result is the union of S1 and S2 Global => null, Post => Is_Union'Result = @@ -167,7 +179,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Global => null, Pre => Iter_Has_Element (S, K); pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem); + private + pragma SPARK_Mode (Off); subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; @@ -192,4 +206,5 @@ private function Iter_Element (S : Set; K : Private_Key) return Element_Type is (Containers.Get (S.Content, Count_Type (K))); + end Ada.Containers.Functional_Sets; diff --git a/gcc/ada/a-cofuve.adb b/gcc/ada/a-cofuve.adb index 6f4f2b131b6..04c79097cae 100644 --- a/gcc/ada/a-cofuve.adb +++ b/gcc/ada/a-cofuve.adb @@ -33,9 +33,6 @@ pragma Ada_2012; package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is use Containers; - pragma Assertion_Policy - (Pre => Suppressible, Ghost => Suppressible, Post => Ignore); - --------- -- "=" -- --------- @@ -66,7 +63,11 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is --------- function Add (S : Sequence; E : Element_Type) return Sequence is - (Content => Add (S.Content, E)); + (Content => Add (S.Content, + Index_Type'Val + (Index_Type'Pos (Index_Type'First) + + Length (S.Content)), + E)); --------- -- Get -- @@ -75,6 +76,16 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is function Get (S : Sequence; N : Extended_Index) return Element_Type is (Get (S.Content, N)); + ------------ + -- Insert -- + ------------ + + function Insert + (S : Sequence; + N : Index_Type; + E : Element_Type) return Sequence is + (Content => Add (S.Content, N, E)); + ------------ -- Is_Add -- ------------ @@ -123,6 +134,13 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is function Length (S : Sequence) return Count_Type is (Length (S.Content)); + ------------ + -- Remove -- + ------------ + + function Remove (S : Sequence; N : Index_Type) return Sequence is + (Content => Remove (S.Content, N)); + --------- -- Set -- --------- diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads index 9d990a9afc3..13c047ed8e1 100644 --- a/gcc/ada/a-cofuve.ads +++ b/gcc/ada/a-cofuve.ads @@ -34,18 +34,20 @@ private with Ada.Containers.Functional_Base; generic type Index_Type is (<>); - -- To avoid Constraint_Error being raised at runtime, Index_Type'Base - -- should have at least one more element at the left than Index_Type. + -- To avoid Constraint_Error being raised at run time, Index_Type'Base + -- should have at least one more element at the low end than Index_Type. type Element_Type (<>) is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Functional_Vectors with SPARK_Mode is + pragma Assertion_Policy (Post => Ignore); + subtype Extended_Index is Index_Type'Base range Index_Type'Pred (Index_Type'First) .. Index_Type'Last; - -- Index_Type with one more element to the left. + -- Index_Type with one more element at the low end of the range. -- This type is never used but it forces GNATprove to check that there is - -- room for one more element at the left of Index_Type. + -- room for one more element at the low end of Index_Type. type Sequence is private with Default_Initial_Condition => Length (Sequence) = 0, @@ -55,9 +57,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Element => Get); -- Sequences are empty when default initialized. -- Quantification over sequences can be done using the regular - -- quantification over its range or directky on its elements using for of. + -- quantification over its range or directly on its elements with "for of". - -- Sequences are axiomatized using Length and Get providing respectively + -- Sequences are axiomatized using Length and Get, providing respectively -- the length of a sequence and an accessor to its Nth element: function Length (S : Sequence) return Count_Type with @@ -73,14 +75,14 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is function First return Extended_Index is (Index_Type'First); function Get (S : Sequence; N : Extended_Index) return Element_Type - -- Get ranges over Extended_Index so that it can be used for iteration. + -- Get ranges over Extended_Index so that it can be used for iteration with Global => null, Pre => N in Index_Type'First .. Last (S); function "=" (S1, S2 : Sequence) return Boolean with - -- Extensional equality over sequences. + -- Extensional equality over sequences Global => null, Post => "="'Result = @@ -109,22 +111,22 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is function Is_Set (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence) return Boolean - -- Returns True if Result is S where the Nth element has been replaced by + -- Returns True if Result is S, where the Nth element has been replaced by -- E. with Global => null, Post => Is_Set'Result = (N in Index_Type'First .. Last (S) - and then Length (Result) = Length (S) - and then Get (Result, N) = E - and then (for all M in Index_Type'First .. Last (S) => - (if M /= N then Get (Result, M) = Get (S, M)))); + and then Length (Result) = Length (S) + and then Get (Result, N) = E + and then (for all M in Index_Type'First .. Last (S) => + (if M /= N then Get (Result, M) = Get (S, M)))); function Set (S : Sequence; N : Index_Type; E : Element_Type) return Sequence - -- Returns S where the Nth element has been replaced by E. - -- Is_Set (S, N, E, Result) should be instead of than + -- Returns S, where the Nth element has been replaced by E. + -- Is_Set (S, N, E, Result) should be used instead of -- Result = Set (S, N, E) whenever possible both for execution and for -- proof. @@ -135,15 +137,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is function Is_Add (S : Sequence; E : Element_Type; Result : Sequence) return Boolean - -- Returns True if Result is S appended with E. + -- Returns True if Result is S appended with E with Global => null, Post => Is_Add'Result = (Length (Result) = Length (S) + 1 - and then Get (Result, Last (Result)) = E - and then (for all M in Index_Type'First .. Last (S) => - Get (Result, M) = Get (S, M))); + and then Get (Result, Last (Result)) = E + and then (for all M in Index_Type'First .. Last (S) => + Get (Result, M) = Get (S, M))); function Add (S : Sequence; E : Element_Type) return Sequence with -- Returns S appended with E. @@ -154,6 +156,39 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Pre => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last, Post => Is_Add (S, E, Add'Result); + function Insert + (S : Sequence; + N : Index_Type; + E : Element_Type) return Sequence + with + -- Returns S with E inserted at index I + + Global => null, + Pre => Length (S) < Count_Type'Last and then Last (S) < Index_Type'Last + and then N <= Extended_Index'Succ (Last (S)), + Post => Length (Insert'Result) = Length (S) + 1 + and then Get (Insert'Result, N) = E + and then (for all M in Index_Type'First .. Extended_Index'Pred (N) => + Get (Insert'Result, M) = Get (S, M)) + and then (for all M in Extended_Index'Succ (N) .. Last (Insert'Result) => + Get (Insert'Result, M) = Get (S, Extended_Index'Pred (M))) + and then (for all M in N .. Last (S) => + Get (Insert'Result, Extended_Index'Succ (M)) = Get (S, M)); + + function Remove (S : Sequence; N : Index_Type) return Sequence with + -- Returns S without the element at index N + + Global => null, + Pre => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last + and N in Index_Type'First .. Last (S), + Post => Length (Remove'Result) = Length (S) - 1 + and then (for all M in Index_Type'First .. Extended_Index'Pred (N) => + Get (Remove'Result, M) = Get (S, M)) + and then (for all M in N .. Last (Remove'Result) => + Get (Remove'Result, M) = Get (S, Extended_Index'Succ (M))) + and then (for all M in Extended_Index'Succ (N) .. Last (S) => + Get (Remove'Result, Extended_Index'Pred (M)) = Get (S, M)); + --------------------------- -- Iteration Primitives -- --------------------------- @@ -172,6 +207,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Pre => Iter_Has_Element (S, I); private + pragma SPARK_Mode (Off); package Containers is new Ada.Containers.Functional_Base @@ -194,5 +230,6 @@ private is (I in Index_Type'First .. (Index_Type'Val - ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))); + ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))); + end Ada.Containers.Functional_Vectors; -- 2.30.2