blob: 521f4bfcab53363e9da33cd766d702f9f73524d6 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
-- --
-- S p e c --
-- --
-- Copyright (C) 2004-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
with Ada.Containers.Functional_Vectors;
with Ada.Containers.Functional_Maps;
generic
type Element_Type is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Doubly_Linked_Lists with
SPARK_Mode
is
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
pragma Assertion_Policy (Pre => Ignore);
pragma Assertion_Policy (Post => Ignore);
pragma Assertion_Policy (Contract_Cases => Ignore);
pragma Annotate (CodePeer, Skip_Analysis);
type List (Capacity : Count_Type) is private with
Iterable => (First => First,
Next => Next,
Has_Element => Has_Element,
Element => Element),
Default_Initial_Condition => Is_Empty (List);
pragma Preelaborable_Initialization (List);
type Cursor is record
Node : Count_Type := 0;
end record;
No_Element : constant Cursor := Cursor'(Node => 0);
Empty_List : constant List;
function Length (Container : List) return Count_Type with
Global => null,
Post => Length'Result <= Container.Capacity;
pragma Unevaluated_Use_Of_Old (Allow);
package Formal_Model with Ghost is
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
package M is new Ada.Containers.Functional_Vectors
(Index_Type => Positive_Count_Type,
Element_Type => Element_Type);
function "="
(Left : M.Sequence;
Right : M.Sequence) return Boolean renames M."=";
function "<"
(Left : M.Sequence;
Right : M.Sequence) return Boolean renames M."<";
function "<="
(Left : M.Sequence;
Right : M.Sequence) return Boolean renames M."<=";
function M_Elements_In_Union
(Container : M.Sequence;
Left : M.Sequence;
Right : M.Sequence) return Boolean
-- The elements of Container are contained in either Left or Right
with
Global => null,
Post =>
M_Elements_In_Union'Result =
(for all I in 1 .. M.Length (Container) =>
(for some J in 1 .. M.Length (Left) =>
Element (Container, I) = Element (Left, J))
or (for some J in 1 .. M.Length (Right) =>
Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
(Left : M.Sequence;
L_Fst : Positive_Count_Type := 1;
L_Lst : Count_Type;
Right : M.Sequence;
R_Fst : Positive_Count_Type := 1;
R_Lst : Count_Type) return Boolean
-- The elements of the slice from L_Fst to L_Lst in Left are contained
-- in the slide from R_Fst to R_Lst in Right.
with
Global => null,
Pre => L_Lst <= M.Length (Left) and R_Lst <= M.Length (Right),
Post =>
M_Elements_Included'Result =
(for all I in L_Fst .. L_Lst =>
(for some J in R_Fst .. R_Lst =>
Element (Left, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
function M_Elements_Reversed
(Left : M.Sequence;
Right : M.Sequence) return Boolean
-- Right is Left in reverse order
with
Global => null,
Post =>
M_Elements_Reversed'Result =
(M.Length (Left) = M.Length (Right)
and (for all I in 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 : Positive_Count_Type;
Y : Positive_Count_Type) return Boolean
-- Elements stored at X and Y are reversed in Left and Right
with
Global => null,
Pre => X <= M.Length (Left) and Y <= M.Length (Left),
Post =>
M_Elements_Swapped'Result =
(M.Length (Left) = M.Length (Right)
and Element (Left, X) = Element (Right, Y)
and Element (Left, Y) = Element (Right, X)
and M.Equal_Except (Left, Right, X, Y));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
Element_Type => Positive_Count_Type,
Equivalent_Keys => "=",
Enable_Handling_Of_Equivalence => False);
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;
Big : P.Map;
Cut : Positive_Count_Type;
Count : Count_Type := 1) return Boolean
with
Global => null,
Post =>
P_Positions_Shifted'Result =
-- Big contains all cursors of Small
(P.Keys_Included (Small, Big)
-- 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 : Cursor;
Y : Cursor) return Boolean
-- Left and Right contain the same cursors, but the positions of X and Y
-- are reversed.
with
Ghost,
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));
function P_Positions_Truncated
(Small : P.Map;
Big : P.Map;
Cut : Positive_Count_Type;
Count : Count_Type := 1) return Boolean
with
Ghost,
Global => null,
Post =>
P_Positions_Truncated'Result =
-- 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));
function Mapping_Preserved
(M_Left : M.Sequence;
M_Right : M.Sequence;
P_Left : P.Map;
P_Right : P.Map) return Boolean
with
Ghost,
Global => null,
Post =>
(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))));
function Model (Container : List) return M.Sequence with
-- The high-level model of a list is a sequence of elements. Cursors are
-- not represented in this model.
Ghost,
Global => null,
Post => M.Length (Model'Result) = Length (Container);
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model);
function Positions (Container : List) return P.Map with
-- The Positions map is used to model cursors. It only contains valid
-- cursors and map them to their position in the container.
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 =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J)));
procedure Lift_Abstraction_Level (Container : List) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
-- assume that we can access to the same elements by iterating over
-- positions or cursors.
-- This information is not generally useful except when switching from
-- a low-level cursor-aware view of a container to a high-level
-- position-based view.
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;
-- 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 "=" (Left, Right : List) return Boolean with
Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function Is_Empty (Container : List) return Boolean with
Global => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out List) with
Global => null,
Post => Length (Container) = 0;
procedure Assign (Target : in out List; Source : List) with
Global => null,
Pre => Target.Capacity >= Length (Source),
Post => Model (Target) = Model (Source);
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);
function Element
(Container : List;
Position : Cursor) return Element_Type
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Element'Result =
Element (Model (Container), P.Get (Positions (Container), Position));
pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out List;
Position : Cursor;
New_Item : Element_Type)
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Length (Container) = Length (Container)'Old
-- Cursors are preserved
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
-- Other elements are preserved
and M.Equal_Except
(Model (Container)'Old,
Model (Container),
P.Get (Positions (Container), Position));
function At_End (E : access constant List) return access constant List
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function At_End
(E : access constant Element_Type) return access constant Element_Type
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function Constant_Reference
(Container : aliased List;
Position : Cursor) return not null access constant Element_Type
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Constant_Reference'Result.all =
Element (Model (Container), P.Get (Positions (Container), Position));
function Reference
(Container : not null access List;
Position : Cursor) return not null access Element_Type
with
Global => null,
Pre => Has_Element (Container.all, Position),
Post =>
Length (Container.all) = Length (At_End (Container).all)
-- Cursors are preserved
and Positions (Container.all) = Positions (At_End (Container).all)
-- Container will have Result.all at position Position
and At_End (Reference'Result).all =
Element (Model (At_End (Container).all),
P.Get (Positions (At_End (Container).all), Position))
-- All other elements are preserved
and M.Equal_Except
(Model (Container.all),
Model (At_End (Container).all),
P.Get (Positions (At_End (Container).all), 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;
procedure Insert
(Container : in out List;
Before : Cursor;
New_Item : Element_Type)
with
Global => null,
Pre =>
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))
-- 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),
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 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
-- 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;
Before : Cursor;
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),
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 (if Count > 0 then
M.Constant_Range
(Container => Model (Container),
Fst => Length (Container)'Old + 1,
Lst => Length (Container),
Item => New_Item))
-- 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));
procedure Insert
(Container : in out List;
Before : Cursor;
New_Item : Element_Type;
Position : out Cursor)
with
Global => null,
Pre =>
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))
-- 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 1
and M.Range_Shifted
(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
-- 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));
procedure Insert
(Container : in out List;
Before : Cursor;
New_Item : Element_Type;
Position : out Cursor;
Count : Count_Type)
with
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 =>
(Count = 0 =>
Position = Before
and Model (Container) = Model (Container)'Old
and Positions (Container) = Positions (Container)'Old,
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
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)
-- 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;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Container.Capacity - Count,
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);
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
-- Positions contains a new mapping from the last cursor of Container
-- to its length.
and 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))
-- 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;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Container.Capacity - Count,
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 (if Count > 0 then
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,
Depends => (Container =>+ Position, Position => null),
Pre => Has_Element (Container, Position),
Post =>
Length (Container) = Length (Container)'Old - 1
-- 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 located after Position are shifted by 1
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => P.Get (Positions (Container)'Old, Position'Old),
Lst => Length (Container),
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;
Position : in out Cursor;
Count : Count_Type)
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Length (Container) in
Length (Container)'Old - Count .. Length (Container)'Old
-- 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),
Contract_Cases =>
-- All the elements after Position have been erased
(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),
others =>
Length (Container) = Length (Container)'Old - Count
-- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => P.Get (Positions (Container)'Old, Position'Old),
Lst => Length (Container),
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),
Right => Model (Container)'Old,
Fst => 1,
Lst => Length (Container),
Offset => 1)
-- 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,
others =>
Length (Container) = Length (Container)'Old - Count
-- Elements of Container are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => 1,
Lst => Length (Container),
Offset => Count)
-- 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 last cursor of Container has been removed
and not P.Has_Key (Positions (Container), Last (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 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) = Length (Container)'Old - Count
-- 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));
procedure Reverse_Elements (Container : in out List) with
Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap
(Container : in out List;
I : Cursor;
J : Cursor)
with
Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post =>
M_Elements_Swapped
(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;
procedure Swap_Links
(Container : in out List;
I : Cursor;
J : Cursor)
with
Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post =>
M_Elements_Swapped
(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);
procedure Splice
(Target : in out List;
Before : Cursor;
Source : in out List)
-- Target and Source should not be aliased
with
Global => null,
Pre =>
Length (Source) <= Target.Capacity - Length (Target)
and then (Has_Element (Target, Before)
or else Before = No_Element),
Post =>
Length (Source) = 0
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_Included
(Left => Model (Source)'Old,
L_Lst => Length (Source)'Old,
Right => Model (Target),
R_Fst => Length (Target)'Old + 1,
R_Lst => Length (Target))
and M_Elements_Included
(Left => Model (Target),
L_Fst => Length (Target)'Old + 1,
L_Lst => Length (Target),
Right => Model (Source)'Old,
R_Lst => Length (Source)'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.
and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Length (Source)'Old,
Right => Model (Target),
R_Fst => P.Get (Positions (Target)'Old, Before),
R_Lst =>
P.Get (Positions (Target)'Old, Before) - 1 +
Length (Source)'Old)
and M_Elements_Included
(Left => Model (Target),
L_Fst => P.Get (Positions (Target)'Old, Before),
L_Lst =>
P.Get (Positions (Target)'Old, Before) - 1 +
Length (Source)'Old,
Right => Model (Source)'Old,
R_Lst => Length (Source)'Old)
-- 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)
-- 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));
procedure Splice
(Target : in out List;
Before : Cursor;
Source : in out List;
Position : in out Cursor)
-- Target and Source should not be aliased
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,
Post =>
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 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)
-- 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;
Before : Cursor;
Position : Cursor)
with
Global => null,
Pre =>
(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 =>
Model (Container) = Model (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),
Fst => 1,
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))
-- 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)),
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)));
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);
function First_Element (Container : List) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
Post => First_Element'Result = M.Get (Model (Container), 1);
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));
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));
function Next (Container : List; Position : Cursor) return Cursor with
Global => null,
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);
procedure Next (Container : List; Position : in out Cursor) with
Global => null,
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);
function Previous (Container : List; Position : Cursor) return Cursor with
Global => null,
Pre =>
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
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);
procedure Previous (Container : List; Position : in out Cursor) with
Global => null,
Pre =>
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
(Position = No_Element
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);
function Find
(Container : List;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
Global => null,
Pre =>
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
-- If Item 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)
=>
Find'Result = No_Element,
-- Otherwise, Find returns a valid cursor 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 result of Find is located after Position
and (if Position /= No_Element then
P.Get (Positions (Container), Find'Result) >=
P.Get (Positions (Container), Position))
-- It is the first occurrence 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;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
Global => null,
Pre =>
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
-- If Item 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)
=>
Reverse_Find'Result = No_Element,
-- Otherwise, Find returns a valid cursor 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 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 occurrence 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;
Item : Element_Type) return Boolean
with
Global => null,
Post =>
Contains'Result = M.Contains (Container => Model (Container),
Fst => 1,
Lst => Length (Container),
Item => Item);
function Has_Element
(Container : List;
Position : Cursor) return Boolean
with
Global => null,
Post =>
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
package Formal_Model with Ghost is
function M_Elements_Sorted (Container : M.Sequence) return Boolean
with
Global => null,
Post =>
M_Elements_Sorted'Result =
(for all I in 1 .. M.Length (Container) =>
(for all J in I .. M.Length (Container) =>
not (Element (Container, J) < Element (Container, I))));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model;
use Formal_Model;
function Is_Sorted (Container : List) return Boolean with
Global => null,
Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
procedure Sort (Container : in out List) with
Global => null,
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Length (Container),
Right => Model (Container),
R_Lst => Length (Container))
and M_Elements_Included
(Left => Model (Container),
L_Lst => Length (Container),
Right => Model (Container)'Old,
R_Lst => Length (Container));
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)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Length (Target)'Old,
Right => Model (Target),
R_Lst => Length (Target))
and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Length (Source)'Old,
Right => Model (Target),
R_Lst => Length (Target))
and M_Elements_In_Union
(Model (Target),
Model (Source)'Old,
Model (Target)'Old);
end Generic_Sorting;
private
pragma SPARK_Mode (Off);
type Node_Type is record
Prev : Count_Type'Base := -1;
Next : Count_Type;
Element : aliased Element_Type;
end record;
function "=" (L, R : Node_Type) return Boolean is abstract;
type Node_Array is array (Count_Type range <>) of Node_Type;
function "=" (L, R : Node_Array) return Boolean is abstract;
type List (Capacity : Count_Type) is record
Free : Count_Type'Base := -1;
Length : Count_Type := 0;
First : Count_Type := 0;
Last : Count_Type := 0;
Nodes : Node_Array (1 .. Capacity);
end record;
Empty_List : constant List := (0, others => <>);
end Ada.Containers.Formal_Doubly_Linked_Lists;