generic
type Element_Type is private;
+
package Ada.Containers.Formal_Doubly_Linked_Lists with
SPARK_Mode
is
package M is new Ada.Containers.Functional_Vectors
(Index_Type => Positive_Count_Type,
Element_Type => Element_Type);
- function "=" (Left, Right : M.Sequence) return Boolean renames M."=";
- function "<" (Left, Right : M.Sequence) return Boolean renames M."<";
- function "<=" (Left, 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 "<="
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean renames M."<=";
function M_Elements_Shuffle
(Left : M.Sequence;
Right : M.Sequence;
Fst : Positive_Count_Type;
Lst : Count_Type;
- Offset : Count_Type'Base)
- return Boolean
+ Offset : Count_Type'Base) return Boolean
-- The slice from Fst to Lst in Left contains the same elements than the
-- same slide shifted by Offset in Right
with
and Offset in 1 - Fst .. M.Length (Right) - Lst,
Post =>
M_Elements_Shuffle'Result =
- (for all J in Fst + Offset .. Lst + Offset =>
- (for some I in Fst .. Lst =>
- Element (Left, I) = Element (Right, J)));
+ (for all J in Fst + Offset .. Lst + Offset =>
+ (for some I in Fst .. Lst =>
+ Element (Left, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shuffle);
- function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean
+ 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 1 .. M.Length (Left) =>
- Element (Left, I)
- = Element (Right, M.Length (Left) - I + 1))
- and
- (for all I in 1 .. M.Length (Left) =>
- Element (Right, I)
- = Element (Left, M.Length (Left) - I + 1)));
+ (M.Length (Left) = M.Length (Right)
+ and (for all I in 1 .. M.Length (Left) =>
+ Element (Left, I) =
+ Element (Right, M.Length (Left) - I + 1))
+ and (for all I in 1 .. M.Length (Left) =>
+ Element (Right, I) =
+ Element (Left, M.Length (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
(Left : M.Sequence;
Right : M.Sequence;
- X, Y : Positive_Count_Type)
- return Boolean
+ X : Positive_Count_Type;
+ Y : Positive_Count_Type) return Boolean
-- Elements stored at X and Y are reversed in Left and Right
with
Global => null,
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));
+ 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);
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
Element_Type => Positive_Count_Type,
Equivalent_Keys => "=");
- function "=" (Left, Right : P.Map) return Boolean renames P."=";
- function "<=" (Left, Right : P.Map) return Boolean renames P."<=";
+
+ function "="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."=";
+
+ function "<="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."<=";
function P_Positions_Shifted
(Small : P.Map;
Post =>
P_Positions_Shifted'Result =
- -- Big contains all cursors of Small
- (P.Keys_Included (Small, Big)
+ -- Big contains all cursors of Small
- -- Cursors located before Cut are not moved, cursors located after
- -- are shifted by Count.
- and
- (for all I of Small =>
- (if P.Get (Small, I) < Cut
- then P.Get (Big, I) = P.Get (Small, I)
- else P.Get (Big, I) - Count = P.Get (Small, I)))
+ P.Keys_Included (Small, Big)
- -- New cursors of Big (if any) are between Cut and Cut - 1 + Count
- and
- (for all I of Big =>
- P.Has_Key (Small, I)
- or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+ -- Cursors located before Cut are not moved, cursors located
+ -- after are shifted by Count.
+
+ and (for all I of Small =>
+ (if P.Get (Small, I) < Cut then
+ P.Get (Big, I) = P.Get (Small, I)
+ else
+ P.Get (Big, I) - Count = P.Get (Small, I)))
+
+ -- New cursors of Big (if any) are between Cut and Cut - 1 +
+ -- Count.
+
+ and (for all I of Big =>
+ P.Has_Key (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1);
function P_Positions_Swapped
(Left : P.Map;
Right : P.Map;
- X, Y : Cursor) return Boolean
+ X : Cursor;
+ Y : Cursor) return Boolean
-- Left and Right contain the same cursors, but the positions of X and Y
-- are reversed.
with
Global => null,
Post =>
P_Positions_Swapped'Result =
- (P.Same_Keys (Left, Right)
- and P.Elements_Equal_Except (Left, Right, X, Y)
- and P.Has_Key (Left, X) and P.Has_Key (Left, Y)
- and P.Get (Left, X) = P.Get (Right, Y)
- and P.Get (Left, Y) = P.Get (Right, X));
+ (P.Same_Keys (Left, Right)
+ and P.Elements_Equal_Except (Left, Right, X, Y)
+ and P.Has_Key (Left, X)
+ and P.Has_Key (Left, Y)
+ and P.Get (Left, X) = P.Get (Right, Y)
+ and P.Get (Left, Y) = P.Get (Right, X));
function P_Positions_Truncated
(Small : P.Map;
Post =>
P_Positions_Truncated'Result =
- -- Big contains all cursors of Small at the same position
- (Small <= Big
+ -- Big contains all cursors of Small at the same position
+
+ (Small <= Big
- -- New cursors of Big (if any) are between Cut and Cut - 1 + Count
- and
- (for all I of Big =>
- P.Has_Key (Small, I)
- or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+ -- New cursors of Big (if any) are between Cut and Cut - 1 +
+ -- Count.
+
+ and (for all I of Big =>
+ P.Has_Key (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
function Mapping_Preserved
(M_Left : M.Sequence;
Ghost,
Global => null,
Post =>
- (if Mapping_Preserved'Result then
+ (if Mapping_Preserved'Result then
-- Left and Right contain the same cursors
+
P.Same_Keys (P_Left, P_Right)
- -- Mappings from cursors to elements induced by M_Left, P_Left
- -- and M_Right, P_Right are the same.
- and (for all C of P_Left =>
- M.Get (M_Left, P.Get (P_Left, C))
- = M.Get (M_Right, P.Get (P_Right, C))));
+ -- Mappings from cursors to elements induced by M_Left, P_Left
+ -- and M_Right, P_Right are the same.
+
+ and (for all C of P_Left =>
+ M.Get (M_Left, P.Get (P_Left, C)) =
+ M.Get (M_Right, P.Get (P_Right, C))));
function Model (Container : List) return M.Sequence with
-- The highlevel model of a list is a sequence of elements. Cursors are
Ghost,
Global => null,
- Post => not P.Has_Key (Positions'Result, No_Element)
- -- Positions of cursors are smaller than the container's length.
- and then
- (for all I of Positions'Result =>
- P.Get (Positions'Result, I) in 1 .. Length (Container)
-
- -- No two cursors have the same position. Note that we do not
- -- state that there is a cursor in the map for each position,
- -- as it is rarely needed.
- and then
- (for all J of Positions'Result =>
+ Post =>
+ not P.Has_Key (Positions'Result, No_Element)
+
+ -- Positions of cursors are smaller than the container's length.
+
+ and then
+ (for all I of Positions'Result =>
+ P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+ -- No two cursors have the same position. Note that we do not
+ -- state that there is a cursor in the map for each position, as
+ -- it is rarely needed.
+
+ and then
+ (for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
- then I = J)));
+ then I = J)));
procedure Lift_Abstraction_Level (Container : List) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
Ghost,
Global => null,
Post =>
- (for all Elt of Model (Container) =>
- (for some I of Positions (Container) =>
- M.Get (Model (Container), P.Get (Positions (Container), I))
- = Elt));
-
- function Element (S : M.Sequence; I : Count_Type) return Element_Type
- renames M.Get;
+ (for all Elt of Model (Container) =>
+ (for some I of Positions (Container) =>
+ M.Get (Model (Container), P.Get (Positions (Container), I)) =
+ Elt));
+
+ function Element
+ (S : M.Sequence;
+ I : Count_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 Copy (Source : List; Capacity : Count_Type := 0) return List with
Global => null,
Pre => Capacity = 0 or else Capacity >= Source.Capacity,
- Post => Model (Copy'Result) = Model (Source)
- and Positions (Copy'Result) = Positions (Source)
- and (if Capacity = 0 then Copy'Result.Capacity = Source.Capacity
- else Copy'Result.Capacity = Capacity);
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Positions (Copy'Result) = Positions (Source)
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Source.Capacity
+ else
+ Copy'Result.Capacity = Capacity);
function Element
(Container : List;
Pre => Has_Element (Container, Position),
Post =>
Element'Result =
- Element (Model (Container),
- P.Get (Positions (Container), Position));
+ Element (Model (Container), P.Get (Positions (Container), Position));
pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
with
Global => null,
Pre => Has_Element (Container, Position),
- Post => Length (Container) = Length (Container)'Old
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Cursors are preserved
- -- Cursors are preserved.
- and Positions (Container)'Old = Positions (Container)
+ and Positions (Container)'Old = Positions (Container)
- -- The element at the position of Position in Container is New_Item
- and Element (Model (Container), P.Get (Positions (Container), Position))
- = New_Item
+ -- The element at the position of Position in Container is New_Item
- -- Other elements are preserved
- and M.Equal_Except (Model (Container)'Old,
- Model (Container),
- P.Get (Positions (Container), Position));
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Position)) = New_Item
+
+ -- Other elements are preserved
+
+ and M.Equal_Except
+ (Model (Container)'Old,
+ Model (Container),
+ P.Get (Positions (Container), Position));
procedure Move (Target : in out List; Source : in out List) with
Global => null,
Pre => Target.Capacity >= Length (Source),
- Post => Model (Target) = Model (Source'Old)
- and Length (Source) = 0;
+ Post => Model (Target) = Model (Source'Old) and Length (Source) = 0;
procedure Insert
(Container : in out List;
with
Global => null,
Pre =>
- Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element),
+ Length (Container) < Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + 1,
Contract_Cases =>
(Before = No_Element =>
-- Positions contains a new mapping from the last cursor of
-- Container to its length.
+
P.Get (Positions (Container), Last (Container)) = Length (Container)
- -- Other cursors come from Container'Old
- and P.Keys_Included_Except
- (Left => Positions (Container),
- Right => Positions (Container)'Old,
- New_Key => Last (Container))
+ -- Other cursors come from Container'Old
+
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
- -- Cursors of Container'Old keep the same position
- and Positions (Container)'Old <= Positions (Container)
+ -- Cursors of Container'Old keep the same position
- -- Model contains a new element New_Item at the end
- and Element (Model (Container), Length (Container)) = New_Item
+ and Positions (Container)'Old <= Positions (Container)
- -- Elements of Container'Old are preserved
- and Model (Container)'Old <= Model (Container),
- others =>
+ -- Model contains a new element New_Item at the end
+
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+
+ and Model (Container)'Old <= Model (Container),
+
+ others =>
+
+ -- The elements of Container located before Before are preserved
- -- The elements of Container located before Before are preserved.
M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container)'Old, Before) - 1)
- -- Other elements are shifted by 1.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Before),
- Lst => Length (Container)'Old,
- Offset => 1)
-
- -- New_Item is stored at the previous position of Before in
- -- Container
- and Element
- (Model (Container), P.Get (Positions (Container)'Old, Before))
- = New_Item
+ -- Other elements are shifted by 1
- -- A new cursor has been inserted at position Before in Container
- and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => P.Get (Positions (Container)'Old, Before)));
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- New_Item is stored at the previous position of Before in
+ -- Container.
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container)'Old, Before)) = New_Item
+
+ -- A new cursor has been inserted at position Before in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container)'Old, Before)));
procedure Insert
(Container : in out List;
New_Item : Element_Type;
Count : Count_Type)
with
- Global => null,
- Pre =>
- Length (Container) <= Container.Capacity - Count
- and then (Has_Element (Container, Before)
- or else Before = No_Element),
+ Global => null,
+ Pre =>
+ Length (Container) <= Container.Capacity - Count
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + Count,
Contract_Cases =>
(Before = No_Element =>
-- The elements of Container are preserved
+
M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old)
- -- Container contains Count times New_Item at the end
- and M.Constant_Range
- (Container => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- Item => New_Item)
-
- -- A Count cursors have been inserted at the end of Container
- and P_Positions_Truncated
- (Positions (Container)'Old,
- Positions (Container),
- Cut => Length (Container)'Old + 1,
- Count => Count),
- others =>
+ -- Container contains Count times New_Item at the end
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item)
+
+ -- A Count cursors have been inserted at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Length (Container)'Old + 1,
+ Count => Count),
+
+ others =>
-- The elements of Container located before Before are preserved
+
M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container)'Old, Before) - 1)
- -- Other elements are shifted by Count.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Before),
- Lst => Length (Container)'Old,
- Offset => Count)
-
- -- Container contains Count times New_Item after position Before
- and M.Constant_Range
- (Container => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Before),
- Lst =>
- P.Get (Positions (Container)'Old, Before) - 1 + Count,
- Item => New_Item)
-
- -- Count cursors have been inserted at position Before in Container
- and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => P.Get (Positions (Container)'Old, Before),
- Count => Count));
+ -- Other elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container contains Count times New_Item after position Before
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst =>
+ P.Get (Positions (Container)'Old, Before) - 1 + Count,
+ Item => New_Item)
+
+ -- Count cursors have been inserted at position Before in
+ -- Container.
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container)'Old, Before),
+ Count => Count));
procedure Insert
(Container : in out List;
with
Global => null,
Pre =>
- Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element),
+ Length (Container) < Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is
-- No_Element.
+
and P.Has_Key (Positions (Container), Position)
- and (if Before = No_Element
- then P.Get (Positions (Container), Position)
- = Length (Container)
- else P.Get (Positions (Container), Position)
- = P.Get (Positions (Container)'Old, Before))
+ and (if Before = No_Element then
+ P.Get (Positions (Container), Position) = Length (Container)
+ else
+ P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container)'Old, Before))
+
+ -- The elements of Container located before Position are preserved
- -- The elements of Container located before Position are preserved.
and M.Range_Equal
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container), Position) - 1)
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by 1
- -- Other elements are shifted by 1.
and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container), Position),
- Lst => Length (Container)'Old,
- Offset => 1)
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => Length (Container)'Old,
+ Offset => 1)
-- New_Item is stored at Position in Container
+
and Element
- (Model (Container), P.Get (Positions (Container), Position))
- = New_Item
+ (Model (Container),
+ P.Get (Positions (Container), Position)) = New_Item
-- A new cursor has been inserted at position Position in Container
+
and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => P.Get (Positions (Container), Position));
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container), Position));
procedure Insert
(Container : in out List;
with
Global => null,
Pre =>
- Length (Container) <= Container.Capacity - Count
- and then (Has_Element (Container, Before)
- or else Before = No_Element),
+ Length (Container) <= Container.Capacity - Count
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + Count,
Contract_Cases =>
- (Count = 0 => Position = Before
- and Model (Container) = Model (Container)'Old
- and Positions (Container) = Positions (Container)'Old,
+ (Count = 0 =>
+ Position = Before
+ and Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ others =>
- others =>
-- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is
-- No_Element.
- P.Has_Key (Positions (Container), Position)
- and (if Before = No_Element
- then P.Get (Positions (Container), Position)
- = Length (Container)'Old + 1
- else P.Get (Positions (Container), Position)
- = P.Get (Positions (Container)'Old, Before))
-
- -- The elements of Container located before Position are preserved.
- and M.Range_Equal
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container), Position) - 1)
-
- -- Other elements are shifted by Count.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container), Position),
- Lst => Length (Container)'Old,
- Offset => Count)
-
- -- Container contains Count times New_Item after position Position
- and M.Constant_Range
- (Container => Model (Container),
- Fst => P.Get (Positions (Container), Position),
- Lst => P.Get (Positions (Container), Position) - 1 + Count,
- Item => New_Item)
-
- -- Count cursor have been inserted at Position in Container
- and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => P.Get (Positions (Container), Position),
- Count => Count));
- procedure Prepend
- (Container : in out List;
- New_Item : Element_Type)
- with
+ P.Has_Key (Positions (Container), Position)
+ and (if Before = No_Element then
+ P.Get (Positions (Container), Position) =
+ Length (Container)'Old + 1
+ else
+ P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container)'Old, Before))
+
+ -- The elements of Container located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container contains Count times New_Item after position Position
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst =>
+ P.Get (Positions (Container), Position) - 1 + Count,
+ Item => New_Item)
+
+ -- Count cursor have been inserted at Position in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container), Position),
+ Count => Count));
+
+ procedure Prepend (Container : in out List; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Container.Capacity,
Post =>
Length (Container) = Length (Container)'Old + 1
- -- Elements are shifted by 1
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => Length (Container)'Old,
- Offset => 1)
+ -- Elements are shifted by 1
- -- New_Item is the first element of Container
- and Element (Model (Container), 1) = New_Item
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old,
+ Offset => 1)
- -- A new cursor has been inserted at the beginning of Container
- and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => 1);
+ -- New_Item is the first element of Container
+
+ and Element (Model (Container), 1) = New_Item
+
+ -- A new cursor has been inserted at the beginning of Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => 1);
procedure Prepend
(Container : in out List;
Post =>
Length (Container) = Length (Container)'Old + Count
- -- Elements are shifted by Count.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => Length (Container)'Old,
- Offset => Count)
-
- -- Container starts with Count times New_Item
- and M.Constant_Range
- (Container => Model (Container),
- Fst => 1,
- Lst => Count,
- Item => New_Item)
-
- -- Count cursors have been inserted at the beginning of Container
- and P_Positions_Shifted
- (Positions (Container)'Old,
- Positions (Container),
- Cut => 1,
- Count => Count);
+ -- Elements are shifted by Count
- procedure Append
- (Container : in out List;
- New_Item : Element_Type)
- with
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container starts with Count times New_Item
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => 1,
+ Lst => Count,
+ Item => New_Item)
+
+ -- Count cursors have been inserted at the beginning of Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => 1,
+ Count => Count);
+
+ procedure Append (Container : in out List; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Container.Capacity,
- Post => Length (Container) = Length (Container)'Old + 1
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
- -- Positions contains a new mapping from the last cursor of
- -- Container to its length.
- and P.Get (Positions (Container), Last (Container))
- = Length (Container)
+ -- Positions contains a new mapping from the last cursor of Container
+ -- to its length.
- -- Other cursors come from Container'Old
- and P.Keys_Included_Except
- (Left => Positions (Container),
- Right => Positions (Container)'Old,
- New_Key => Last (Container))
+ and P.Get (Positions (Container), Last (Container)) =
+ Length (Container)
- -- Cursors of Container'Old keep the same position
- and Positions (Container)'Old <= Positions (Container)
+ -- Other cursors come from Container'Old
- -- Model contains a new element New_Item at the end
- and Element (Model (Container), Length (Container)) = New_Item
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
- -- Elements of Container'Old are preserved
- and Model (Container)'Old <= Model (Container);
+ -- Cursors of Container'Old keep the same position
+
+ and Positions (Container)'Old <= Positions (Container)
+
+ -- Model contains a new element New_Item at the end
+
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+
+ and Model (Container)'Old <= Model (Container);
procedure Append
(Container : in out List;
Post =>
Length (Container) = Length (Container)'Old + Count
- -- The elements of Container are preserved
- and Model (Container)'Old <= Model (Container)
-
- -- Container contains Count times New_Item at the end
- and M.Constant_Range
- (Container => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- Item => New_Item)
-
- -- Count cursors have been inserted at the end of Container
- and P_Positions_Truncated
- (Positions (Container)'Old,
- Positions (Container),
- Cut => Length (Container)'Old + 1,
- Count => Count);
+ -- The elements of Container are preserved
- procedure Delete
- (Container : in out List;
- Position : in out Cursor)
- with
+ and Model (Container)'Old <= Model (Container)
+
+ -- Container contains Count times New_Item at the end
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item)
+
+ -- Count cursors have been inserted at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Length (Container)'Old + 1,
+ Count => Count);
+
+ procedure Delete (Container : in out List; Position : in out Cursor) with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Length (Container) = Length (Container)'Old - 1
- -- Position is set to No_Element
- and Position = No_Element
+ -- Position is set to No_Element
- -- The elements of Container located before Position are preserved.
- and M.Range_Equal
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+ and Position = No_Element
- -- The elements located after Position are shifted by 1
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
- Lst => Length (Container)'Old,
- Offset => -1)
+ -- The elements of Container located before Position are preserved.
- -- Position has been removed from Container
- and P_Positions_Shifted
- (Positions (Container),
- Positions (Container)'Old,
- Cut => P.Get (Positions (Container)'Old, Position'Old));
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
+ Lst => Length (Container)'Old,
+ Offset => -1)
+
+ -- Position has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old));
procedure Delete
(Container : in out List;
Global => null,
Pre => Has_Element (Container, Position),
Post =>
- Length (Container) in Length (Container)'Old - Count
- .. Length (Container)'Old
+ Length (Container) in
+ Length (Container)'Old - Count .. Length (Container)'Old
- -- Position is set to No_Element
- and Position = No_Element
+ -- Position is set to No_Element
+
+ and Position = No_Element
+
+ -- The elements of Container located before Position are preserved.
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
- -- The elements of Container located before Position are preserved.
- and M.Range_Equal
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
Contract_Cases =>
-- All the elements after Position have been erased
- (Length (Container) - Count < P.Get (Positions (Container), Position)
- =>
+ (Length (Container) - Count < P.Get (Positions (Container), Position) =>
Length (Container) =
P.Get (Positions (Container)'Old, Position'Old) - 1
- -- At most Count cursors have been removed at the end of Container
- and P_Positions_Truncated
- (Positions (Container),
- Positions (Container)'Old,
- Cut => P.Get (Positions (Container)'Old, Position'Old),
- Count => Count),
+ -- At most Count cursors have been removed at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old),
+ Count => Count),
+
others =>
Length (Container) = Length (Container)'Old - Count
- -- Other elements are shifted by Count
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst =>
- P.Get (Positions (Container)'Old, Position'Old) + Count,
- Lst => Length (Container)'Old,
- Offset => -Count)
-
- -- Count cursors have been removed from Container at Position
- and P_Positions_Shifted
- (Positions (Container),
- Positions (Container)'Old,
- Cut => P.Get (Positions (Container)'Old, Position'Old),
- Count => Count));
+ -- Other elements are shifted by Count
- procedure Delete_First (Container : in out List)
- with
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst =>
+ P.Get (Positions (Container)'Old, Position'Old) + Count,
+ Lst => Length (Container)'Old,
+ Offset => -Count)
+
+ -- Count cursors have been removed from Container at Position
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old),
+ Count => Count));
+
+ procedure Delete_First (Container : in out List) with
Global => null,
Pre => not Is_Empty (Container),
Post =>
Length (Container) = Length (Container)'Old - 1
- -- The elements of Container are shifted by 1
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => 2,
- Lst => Length (Container)'Old,
- Offset => -1)
+ -- The elements of Container are shifted by 1
- -- The first cursor of Container has been removed
- and P_Positions_Shifted
- (Positions (Container),
- Positions (Container)'Old,
- Cut => 1);
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 2,
+ Lst => Length (Container)'Old,
+ Offset => -1)
- procedure Delete_First
- (Container : in out List;
- Count : Count_Type)
- with
+ -- The first cursor of Container has been removed
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => 1);
+
+ procedure Delete_First (Container : in out List; Count : Count_Type) with
Global => null,
Contract_Cases =>
-- All the elements of Container have been erased
- (Length (Container) <= Count => Length (Container) = 0,
+
+ (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)'Old,
- Right => Model (Container),
- Fst => Count + 1,
- Lst => Length (Container)'Old,
- Offset => -Count)
+ -- Elements of Container are shifted by Count
- -- The first Count cursors have been removed from Container
- and P_Positions_Shifted
- (Positions (Container),
- Positions (Container)'Old,
- Cut => 1,
- Count => Count));
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => Count + 1,
+ Lst => Length (Container)'Old,
+ Offset => -Count)
- procedure Delete_Last (Container : in out List)
- with
+ -- The first Count cursors have been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => 1,
+ Count => Count));
+
+ procedure Delete_Last (Container : in out List) with
Global => null,
Pre => not Is_Empty (Container),
Post =>
Length (Container) = Length (Container)'Old - 1
- -- The elements of Container are preserved.
- and Model (Container) <= Model (Container)'Old
+ -- The elements of Container are preserved
- -- The last cursor of Container has been removed
- and not P.Has_Key (Positions (Container), Last (Container)'Old)
+ and Model (Container) <= Model (Container)'Old
- -- Other cursors are still valid
- and P.Keys_Included_Except
- (Left => Positions (Container)'Old,
- Right => Positions (Container)'Old,
- New_Key => Last (Container)'Old)
+ -- The last cursor of Container has been removed
- -- The positions of other cursors are preserved
- and Positions (Container) <= Positions (Container)'Old;
+ and not P.Has_Key (Positions (Container), Last (Container)'Old)
- procedure Delete_Last
- (Container : in out List;
- Count : Count_Type)
- with
- Global => null,
+ -- Other cursors are still valid
+
+ and P.Keys_Included_Except
+ (Left => Positions (Container)'Old,
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container)'Old)
+
+ -- The positions of other cursors are preserved
+
+ and Positions (Container) <= Positions (Container)'Old;
+
+ procedure Delete_Last (Container : in out List; 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) <= Count =>
+ Length (Container) = 0,
+
+ others =>
Length (Container) = Length (Container)'Old - Count
- -- The elements of Container are preserved.
- and Model (Container) <= Model (Container)'Old
+ -- The elements of Container are preserved
+
+ and Model (Container) <= Model (Container)'Old
- -- At most Count cursors have been removed at the end of Container
- and P_Positions_Truncated
- (Positions (Container),
- Positions (Container)'Old,
- Cut => Length (Container) + 1,
- Count => Count));
+ -- At most Count cursors have been removed at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Length (Container) + 1,
+ Count => Count));
procedure Reverse_Elements (Container : in out List) with
Global => null,
procedure Swap
(Container : in out List;
- I, J : Cursor)
+ I : Cursor;
+ J : Cursor)
with
Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
(Model (Container)'Old, Model (Container),
X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J))
- and Positions (Container) = Positions (Container)'Old;
+
+ and Positions (Container) = Positions (Container)'Old;
procedure Swap_Links
(Container : in out List;
- I, J : Cursor)
+ I : Cursor;
+ J : Cursor)
with
Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
(Model (Container'Old), Model (Container),
X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J))
- and P_Positions_Swapped
- (Positions (Container)'Old, Positions (Container), I, J);
+ and P_Positions_Swapped
+ (Positions (Container)'Old, Positions (Container), I, J);
procedure Splice
(Target : in out List;
with
Global => null,
Pre =>
- Length (Source) <= Target.Capacity - Length (Target)
+ Length (Source) <= Target.Capacity - Length (Target)
and then (Has_Element (Target, Before)
- or else Before = No_Element),
+ or else Before = No_Element),
Post =>
Length (Source) = 0
- and Length (Target) = Length (Target)'Old + Length (Source)'Old,
+ and Length (Target) = Length (Target)'Old + Length (Source)'Old,
Contract_Cases =>
(Before = No_Element =>
-- The elements of Target are preserved
+
M.Range_Equal
(Left => Model (Target)'Old,
Right => Model (Target),
Fst => 1,
Lst => Length (Target)'Old)
- -- The elements of Source are appended to target, the order is not
- -- specified.
- and M_Elements_Shuffle
- (Left => Model (Source)'Old,
- Right => Model (Target),
- Fst => 1,
- Lst => Length (Source)'Old,
- Offset => Length (Target)'Old)
-
- -- Cursors have been inserted at the end of Target
- and P_Positions_Truncated
- (Positions (Target)'Old,
- Positions (Target),
- Cut => Length (Target)'Old + 1,
- Count => Length (Source)'Old),
- others =>
+ -- The elements of Source are appended to target, the order is not
+ -- specified.
+
+ and M_Elements_Shuffle
+ (Left => Model (Source)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => Length (Source)'Old,
+ Offset => Length (Target)'Old)
+
+ -- Cursors have been inserted at the end of Target
+
+ and P_Positions_Truncated
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => Length (Target)'Old + 1,
+ Count => Length (Source)'Old),
+
+ others =>
-- The elements of Target located before Before are preserved
+
M.Range_Equal
(Left => Model (Target)'Old,
Right => Model (Target),
Fst => 1,
Lst => P.Get (Positions (Target)'Old, Before) - 1)
- -- The elements of Source are inserted before Before, the order is
- -- not specified.
+ -- The elements of Source are inserted before Before, the order is
+ -- not specified.
+
and M_Elements_Shuffle
- (Left => Model (Source)'Old,
- Right => Model (Target),
- Fst => 1,
- Lst => Length (Source)'Old,
- Offset => P.Get (Positions (Target)'Old, Before) - 1)
+ (Left => Model (Source)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => Length (Source)'Old,
+ Offset => P.Get (Positions (Target)'Old, Before) - 1)
-- Other elements are shifted by the length of Source
+
and M.Range_Shifted
- (Left => Model (Target)'Old,
- Right => Model (Target),
- Fst => P.Get (Positions (Target)'Old, Before),
- Lst => Length (Target)'Old,
- Offset => Length (Source)'Old)
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => P.Get (Positions (Target)'Old, Before),
+ Lst => Length (Target)'Old,
+ Offset => Length (Source)'Old)
-- Cursors have been inserted at position Before in Target
+
and P_Positions_Shifted
- (Positions (Target)'Old,
- Positions (Target),
- Cut => P.Get (Positions (Target)'Old, Before),
- Count => Length (Source)'Old));
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => P.Get (Positions (Target)'Old, Before),
+ Count => Length (Source)'Old));
procedure Splice
(Target : in out List;
with
Global => null,
Pre =>
- (Has_Element (Target, Before)
- or else Before = No_Element)
- and then Has_Element (Source, Position)
- and then Length (Target) < Target.Capacity,
+ (Has_Element (Target, Before) or else Before = No_Element)
+ and then Has_Element (Source, Position)
+ and then Length (Target) < Target.Capacity,
Post =>
- Length (Target) = Length (Target)'Old + 1
- and Length (Source) = Length (Source)'Old - 1
+ Length (Target) = Length (Target)'Old + 1
+ and Length (Source) = Length (Source)'Old - 1
- -- The elements of Source located before Position are preserved.
- and M.Range_Equal
- (Left => Model (Source)'Old,
- Right => Model (Source),
- Fst => 1,
- Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
+ -- The elements of Source located before Position are preserved
- -- The elements located after Position are shifted by 1
- and M.Range_Shifted
- (Left => Model (Source)'Old,
- Right => Model (Source),
- Fst => P.Get (Positions (Source)'Old, Position'Old) + 1,
- Lst => Length (Source)'Old,
- Offset => -1)
+ and M.Range_Equal
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
+ Fst => 1,
+ Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
- -- Position has been removed from Source
- and P_Positions_Shifted
- (Positions (Source),
- Positions (Source)'Old,
- Cut => P.Get (Positions (Source)'Old, Position'Old))
+ -- The elements located after Position are shifted by 1
- -- Positions is valid in Target and it is located either before
- -- Before if it is valid in Target or at the end if it is
- -- No_Element.
- and P.Has_Key (Positions (Target), Position)
- and (if Before = No_Element
- then P.Get (Positions (Target), Position)
- = Length (Target)
- else P.Get (Positions (Target), Position)
- = P.Get (Positions (Target)'Old, Before))
-
- -- The elements of Target located before Position are preserved.
- and M.Range_Equal
- (Left => Model (Target)'Old,
- Right => Model (Target),
- Fst => 1,
- Lst => P.Get (Positions (Target), Position) - 1)
+ and M.Range_Shifted
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
+ Fst => P.Get (Positions (Source)'Old, Position'Old) + 1,
+ Lst => Length (Source)'Old,
+ Offset => -1)
- -- Other elements are shifted by 1.
- and M.Range_Shifted
- (Left => Model (Target)'Old,
- Right => Model (Target),
- Fst => P.Get (Positions (Target), Position),
- Lst => Length (Target)'Old,
- Offset => 1)
-
- -- The element located at Position in Source is moved to Target
- and Element (Model (Target), P.Get (Positions (Target), Position))
- = Element (Model (Source)'Old,
- P.Get (Positions (Source)'Old, Position'Old))
-
- -- A new cursor has been inserted at position Position in Target
- and P_Positions_Shifted
- (Positions (Target)'Old,
- Positions (Target),
- Cut => P.Get (Positions (Target), Position));
+ -- Position has been removed from Source
+
+ and P_Positions_Shifted
+ (Positions (Source),
+ Positions (Source)'Old,
+ Cut => P.Get (Positions (Source)'Old, Position'Old))
+
+ -- Positions is valid in Target and it is located either before
+ -- Before if it is valid in Target or at the end if it is No_Element.
+
+ and P.Has_Key (Positions (Target), Position)
+ and (if Before = No_Element then
+ P.Get (Positions (Target), Position) = Length (Target)
+ else
+ P.Get (Positions (Target), Position) =
+ P.Get (Positions (Target)'Old, Before))
+
+ -- The elements of Target located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target), Position) - 1)
+
+ -- Other elements are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => P.Get (Positions (Target), Position),
+ Lst => Length (Target)'Old,
+ Offset => 1)
+
+ -- The element located at Position in Source is moved to Target
+
+ and Element (Model (Target), P.Get (Positions (Target), Position)) =
+ Element (Model (Source)'Old,
+ P.Get (Positions (Source)'Old, Position'Old))
+
+ -- A new cursor has been inserted at position Position in Target
+
+ and P_Positions_Shifted
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => P.Get (Positions (Target), Position));
procedure Splice
(Container : in out List;
with
Global => null,
Pre =>
- (Has_Element (Container, Before) or else Before = No_Element)
+ (Has_Element (Container, Before) or else Before = No_Element)
and then Has_Element (Container, Position),
Post => Length (Container) = Length (Container)'Old,
Contract_Cases =>
- (Before = Position =>
+ (Before = Position =>
Model (Container) = Model (Container)'Old
- and Positions (Container) = Positions (Container)'Old,
+ and Positions (Container) = Positions (Container)'Old,
Before = No_Element =>
-- The elements located before Position are preserved
+
M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Lst => P.Get (Positions (Container)'Old, Position) - 1)
-- The elements located after Position are shifted by 1
+
and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Position) + 1,
- Lst => Length (Container)'Old,
- Offset => -1)
-
- -- The last element of Container is the one that was previously
- -- at Position.
- and Element (Model (Container), Length (Container))
- = Element (Model (Container)'Old,
- P.Get (Positions (Container)'Old, Position))
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position) + 1,
+ Lst => Length (Container)'Old,
+ Offset => -1)
+
+ -- The last element of Container is the one that was previously at
+ -- Position.
+
+ and Element (Model (Container), Length (Container)) =
+ Element (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
-- Cursors from Container continue designating the same elements
+
and Mapping_Preserved
- (M_Left => Model (Container)'Old,
- M_Right => Model (Container),
- P_Left => Positions (Container)'Old,
- P_Right => Positions (Container)),
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)),
- others =>
+ others =>
-- The elements located before Position and Before are preserved
+
M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
- Lst => Count_Type'Min
- (P.Get (Positions (Container)'Old, Position) - 1,
- P.Get (Positions (Container)'Old, Before) - 1))
-
- -- The elements located after Position and Before are preserved
- and M.Range_Equal
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => Count_Type'Max
- (P.Get (Positions (Container)'Old, Position) + 1,
- P.Get (Positions (Container)'Old, Before) + 1),
- Lst => Length (Container))
-
- -- The elements located after Before and before Position are shifted
- -- by 1 to the right.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Before) + 1,
- Lst => P.Get (Positions (Container)'Old, Position) - 1,
- Offset => 1)
-
- -- The elements located after Position and before Before are shifted
- -- by 1 to the left.
- and M.Range_Shifted
- (Left => Model (Container)'Old,
- Right => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Position) + 1,
- Lst => P.Get (Positions (Container)'Old, Before) - 1,
- Offset => -1)
-
- -- The element previously at Position is now before Before
- and Element (Model (Container),
- P.Get (Positions (Container)'Old, Before))
- = Element (Model (Container)'Old,
- P.Get (Positions (Container)'Old, Position))
-
- -- Cursors from Container continue designating the same elements
- and Mapping_Preserved
- (M_Left => Model (Container)'Old,
- M_Right => Model (Container),
- P_Left => Positions (Container)'Old,
- P_Right => Positions (Container)));
+ Lst =>
+ Count_Type'Min
+ (P.Get (Positions (Container)'Old, Position) - 1,
+ P.Get (Positions (Container)'Old, Before) - 1))
+
+ -- The elements located after Position and Before are preserved
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst =>
+ Count_Type'Max
+ (P.Get (Positions (Container)'Old, Position) + 1,
+ P.Get (Positions (Container)'Old, Before) + 1),
+ Lst => Length (Container))
+
+ -- The elements located after Before and before Position are
+ -- shifted by 1 to the right.
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before) + 1,
+ Lst => P.Get (Positions (Container)'Old, Position) - 1,
+ Offset => 1)
+
+ -- The elements located after Position and before Before are
+ -- shifted by 1 to the left.
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position) + 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1,
+ Offset => -1)
+
+ -- The element previously at Position is now before Before
+
+ and Element (Model (Container),
+ P.Get (Positions (Container)'Old, Before)) =
+ Element (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
+
+ -- Cursors from Container continue designating the same elements
+
+ and Mapping_Preserved
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)));
function First (Container : List) return Cursor with
Global => null,
Contract_Cases =>
- (Length (Container) = 0 => First'Result = No_Element,
- others => Has_Element (Container, First'Result)
- and P.Get (Positions (Container), First'Result) = 1);
+ (Length (Container) = 0 =>
+ First'Result = No_Element,
+
+ others =>
+ Has_Element (Container, First'Result)
+ and P.Get (Positions (Container), First'Result) = 1);
function First_Element (Container : List) return Element_Type with
Global => null,
function Last (Container : List) return Cursor with
Global => null,
Contract_Cases =>
- (Length (Container) = 0 => Last'Result = No_Element,
- others => Has_Element (Container, Last'Result)
- and P.Get (Positions (Container), Last'Result) = Length (Container));
+ (Length (Container) = 0 =>
+ Last'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Last'Result)
+ and P.Get (Positions (Container), Last'Result) =
+ Length (Container));
function Last_Element (Container : List) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
- Post => Last_Element'Result
- = M.Get (Model (Container), Length (Container));
+ Post =>
+ Last_Element'Result = M.Get (Model (Container), Length (Container));
function Next (Container : List; Position : Cursor) return Cursor with
Global => null,
- Pre => Has_Element (Container, Position)
- or else Position = No_Element,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
- or else P.Get (Positions (Container), Position) = Length (Container) =>
- Next'Result = No_Element,
- others => Has_Element (Container, Next'Result)
- and then P.Get (Positions (Container), Next'Result) =
- P.Get (Positions (Container), Position) + 1);
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Next'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Next'Result)
+ and then P.Get (Positions (Container), Next'Result) =
+ P.Get (Positions (Container), Position) + 1);
procedure Next (Container : List; Position : in out Cursor) with
Global => null,
- Pre => Has_Element (Container, Position)
- or else Position = No_Element,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
- or else P.Get (Positions (Container), Position) = Length (Container) =>
- Position = No_Element,
- others => Has_Element (Container, Position)
- and then P.Get (Positions (Container), Position) =
- P.Get (Positions (Container), Position'Old) + 1);
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) + 1);
function Previous (Container : List; Position : Cursor) return Cursor with
Global => null,
- Pre => Has_Element (Container, Position)
- or else Position = No_Element,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
- or else P.Get (Positions (Container), Position) = 1 =>
+ or else P.Get (Positions (Container), Position) = 1
+ =>
Previous'Result = No_Element,
+
others =>
Has_Element (Container, Previous'Result)
- and then P.Get (Positions (Container), Previous'Result) =
- P.Get (Positions (Container), Position) - 1);
+ and then P.Get (Positions (Container), Previous'Result) =
+ P.Get (Positions (Container), Position) - 1);
procedure Previous (Container : List; Position : in out Cursor) with
Global => null,
- Pre => Has_Element (Container, Position)
- or else Position = No_Element,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
- or else P.Get (Positions (Container), Position) = 1 =>
+ or else P.Get (Positions (Container), Position) = 1
+ =>
Position = No_Element,
+
others =>
Has_Element (Container, Position)
- and then P.Get (Positions (Container), Position) =
- P.Get (Positions (Container), Position'Old) - 1);
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) - 1);
function Find
(Container : List;
with
Global => null,
Pre =>
- Has_Element (Container, Position) or else Position = No_Element,
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
-- If Item is not is not contained in Container after Position, Find
-- returns No_Element.
+
(not M.Contains
- (Container => Model (Container),
- Fst => (if Position = No_Element then 1
- else P.Get (Positions (Container), Position)),
- Lst => Length (Container),
- Item => Item)
+ (Container => Model (Container),
+ Fst =>
+ (if Position = No_Element then
+ 1
+ else
+ P.Get (Positions (Container), Position)),
+ Lst => Length (Container),
+ Item => Item)
=>
Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container
+
others =>
P.Has_Key (Positions (Container), Find'Result)
- -- The element designated by the result of Find is Item
- and Element (Model (Container),
- P.Get (Positions (Container), Find'Result)) = Item
+ -- The element designated by the result of Find is Item
+
+ and Element (Model (Container),
+ P.Get (Positions (Container), Find'Result)) = Item
- -- The result of Find is located after Position
- and (if Position /= No_Element
- then P.Get (Positions (Container), Find'Result)
- >= P.Get (Positions (Container), Position))
+ -- The result of Find is located after Position
- -- It is the first occurence of Item in this slice
- and not M.Contains
- (Container => Model (Container),
- Fst => (if Position = No_Element then 1
- else P.Get (Positions (Container), Position)),
- Lst => P.Get (Positions (Container), Find'Result) - 1,
- Item => Item));
+ and (if Position /= No_Element then
+ P.Get (Positions (Container), Find'Result) >=
+ P.Get (Positions (Container), Position))
+
+ -- It is the first occurence of Item in this slice
+
+ and not M.Contains
+ (Container => Model (Container),
+ Fst =>
+ (if Position = No_Element then
+ 1
+ else
+ P.Get (Positions (Container), Position)),
+ Lst =>
+ P.Get (Positions (Container), Find'Result) - 1,
+ Item => Item));
function Reverse_Find
(Container : List;
with
Global => null,
Pre =>
- Has_Element (Container, Position) or else Position = No_Element,
+ Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
-- If Item is not is not contained in Container before Position, Find
-- returns No_Element.
+
(not M.Contains
- (Container => Model (Container),
- Fst => 1,
- Lst => (if Position = No_Element then Length (Container)
- else P.Get (Positions (Container), Position)),
- Item => Item)
+ (Container => Model (Container),
+ Fst => 1,
+ Lst =>
+ (if Position = No_Element then
+ Length (Container)
+ else
+ P.Get (Positions (Container), Position)),
+ Item => Item)
=>
Reverse_Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container
+
others =>
P.Has_Key (Positions (Container), Reverse_Find'Result)
- -- The element designated by the result of Find is Item
- and Element (Model (Container),
- P.Get (Positions (Container), Reverse_Find'Result)) = Item
+ -- The element designated by the result of Find is Item
- -- The result of Find is located before Position
- and (if Position /= No_Element
- then P.Get (Positions (Container), Reverse_Find'Result)
- <= P.Get (Positions (Container), Position))
+ and Element (Model (Container),
+ P.Get (Positions (Container),
+ Reverse_Find'Result)) = Item
- -- It is the last occurence of Item in this slice
- and not M.Contains
- (Container => Model (Container),
- Fst => P.Get (Positions (Container), Reverse_Find'Result) + 1,
- Lst => (if Position = No_Element then Length (Container)
- else P.Get (Positions (Container), Position)),
- Item => Item));
+ -- The result of Find is located before Position
+
+ and (if Position /= No_Element then
+ P.Get (Positions (Container), Reverse_Find'Result) <=
+ P.Get (Positions (Container), Position))
+
+ -- It is the last occurence of Item in this slice
+
+ and not M.Contains
+ (Container => Model (Container),
+ Fst =>
+ P.Get (Positions (Container),
+ Reverse_Find'Result) + 1,
+ Lst =>
+ (if Position = No_Element then
+ Length (Container)
+ else
+ P.Get (Positions (Container), Position)),
+ Item => Item));
function Contains
(Container : List;
with
Global => null,
Post =>
- Contains'Result = M.Contains (Container => Model (Container),
- Fst => 1,
- Lst => Length (Container),
- Item => Item);
+ Contains'Result = M.Contains (Container => Model (Container),
+ Fst => 1,
+ Lst => Length (Container),
+ Item => Item);
- function Has_Element (Container : List; Position : Cursor) return Boolean
+ function Has_Element
+ (Container : List;
+ Position : Cursor) return Boolean
with
Global => null,
Post =>
- Has_Element'Result = P.Has_Key (Positions (Container), Position);
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
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
function M_Elements_Sorted (Container : M.Sequence) return Boolean with
Ghost,
Global => null,
- Post => M_Elements_Sorted'Result =
- (for all I in 1 .. M.Length (Container) =>
- (for all J in I + 1 .. M.Length (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
+ Post =>
+ M_Elements_Sorted'Result =
+ (for all I in 1 .. M.Length (Container) =>
+ (for all J in I + 1 .. M.Length (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : List) return Boolean with
procedure Sort (Container : in out List) with
Global => null,
- Post => Length (Container) = Length (Container)'Old
- and M_Elements_Sorted (Model (Container));
+ Post =>
+ Length (Container) = Length (Container)'Old
+ and M_Elements_Sorted (Model (Container));
- procedure Merge (Target, Source : in out List) with
+ procedure Merge (Target : in out List; Source : in out List) with
-- Target and Source should not be aliased
Global => null,
Pre => Length (Source) <= Target.Capacity - 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)));
+ 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)));
end Generic_Sorting;
private
projects / gcc.git / commitdiff