a-cofuba.ads (Add): Take as an additional input parameter the position where the element should be...
2017-04-27 Claire Dross <dross@adacore.com> * 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
This commit is contained in:
Claire Dross
Arnaud Charlet
parent
11775988d5
commit
394fa9f54a
9 changed files with 227 additions and 105 deletions
|
|
@ -1,3 +1,15 @@
|
|||
2017-04-27 Claire Dross <dross@adacore.com>
|
||||
|
||||
* 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 <kirtchev@adacore.com>
|
||||
|
||||
* checks.adb (Generate_Range_Check): Revert previous change.
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -28,16 +28,16 @@
|
|||
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
||||
-- <http://www.gnu.org/licenses/>. --
|
||||
------------------------------------------------------------------------------
|
||||
-- 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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
---------
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 --
|
||||
-----------
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 --
|
||||
---------
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue