--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_DOUBLY_LINKED_LISTS --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022-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.Unchecked_Deallocation;
+
+with Ada.Containers.Stable_Sorting; use Ada.Containers.Stable_Sorting;
+
+with System; use type System.Address;
+
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
+package body Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists with
+ SPARK_Mode => Off
+is
+ -- Convert Count_Type to Big_Integer
+
+ package Conversions is new Signed_Conversions (Int => Count_Type);
+ use Conversions;
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ procedure Allocate
+ (Container : in out List;
+ New_Item : Element_Type;
+ New_Node : out Count_Type);
+
+ procedure Allocate
+ (Container : in out List;
+ New_Node : out Count_Type);
+
+ procedure Free (Container : in out List; X : Count_Type);
+
+ procedure Insert_Internal
+ (Container : in out List;
+ Before : Count_Type;
+ New_Node : Count_Type);
+
+ function Vet (L : List; Position : Cursor) return Boolean with Inline;
+
+ procedure Resize (Container : in out List) with
+ -- Add more room in the internal array
+
+ Global => null,
+ Pre => Container.Nodes = null
+ or else Length (Container) = Container.Nodes'Length,
+ Post => Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old;
+
+ procedure Finalize_Element is new Ada.Unchecked_Deallocation
+ (Object => Element_Type,
+ Name => Element_Access);
+
+ procedure Finalize_Nodes is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ ---------
+ -- "=" --
+ ---------
+
+ function "=" (Left : List; Right : List) return Boolean is
+ LI : Count_Type;
+ RI : Count_Type;
+
+ begin
+ if Left'Address = Right'Address then
+ return True;
+ end if;
+
+ if Left.Length /= Right.Length then
+ return False;
+ end if;
+
+ LI := Left.First;
+ RI := Right.First;
+ while LI /= 0 loop
+ if Left.Nodes (LI).Element.all /= Right.Nodes (RI).Element.all then
+ return False;
+ end if;
+
+ LI := Left.Nodes (LI).Next;
+ RI := Right.Nodes (RI).Next;
+ end loop;
+
+ return True;
+ end "=";
+
+ ------------
+ -- Adjust --
+ ------------
+
+ overriding procedure Adjust (Container : in out List) is
+ N_Src : Node_Array_Access renames Container.Nodes;
+ N_Tar : Node_Array_Access;
+
+ begin
+ if N_Src = null then
+ return;
+ end if;
+
+ if Container.Length = 0 then
+ Container.Nodes := null;
+ Container.Free := -1;
+ return;
+ end if;
+
+ N_Tar := new Node_Array (1 .. N_Src'Length);
+
+ for X in 1 .. Count_Type (N_Src'Length) loop
+ N_Tar (X) := N_Src (X);
+ if N_Src (X).Element /= null
+ then
+ N_Tar (X).Element := new Element_Type'(N_Src (X).Element.all);
+ end if;
+ end loop;
+
+ N_Src := N_Tar;
+
+ end Adjust;
+
+ --------------
+ -- Allocate --
+ --------------
+
+ procedure Allocate
+ (Container : in out List;
+ New_Node : out Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Container.Nodes = null
+ or else Length (Container) = Container.Nodes'Length
+ then
+ Resize (Container);
+ end if;
+
+ if Container.Free >= 0 then
+ New_Node := Container.Free;
+ Container.Free := N (New_Node).Next;
+ else
+ New_Node := abs Container.Free;
+ Container.Free := Container.Free - 1;
+ end if;
+
+ N (New_Node).Element := null;
+ end Allocate;
+
+ procedure Allocate
+ (Container : in out List;
+ New_Item : Element_Type;
+ New_Node : out Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ Allocate (Container, New_Node);
+
+ N (New_Node).Element := new Element_Type'(New_Item);
+ end Allocate;
+
+ ------------
+ -- Append --
+ ------------
+
+ procedure Append (Container : in out List; New_Item : Element_Type) is
+ begin
+ Insert (Container, No_Element, New_Item, 1);
+ end Append;
+
+ procedure Append
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ begin
+ Insert (Container, No_Element, New_Item, Count);
+ end Append;
+
+ ------------
+ -- Assign --
+ ------------
+
+ procedure Assign (Target : in out List; Source : List) is
+ N : Node_Array_Access renames Source.Nodes;
+ J : Count_Type;
+
+ begin
+ if Target'Address = Source'Address then
+ return;
+ end if;
+
+ Clear (Target);
+
+ J := Source.First;
+ while J /= 0 loop
+ Append (Target, N (J).Element.all);
+ J := N (J).Next;
+ end loop;
+ end Assign;
+
+ -----------
+ -- Clear --
+ -----------
+
+ procedure Clear (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Container.Length = 0 then
+ pragma Assert (Container.First = 0);
+ pragma Assert (Container.Last = 0);
+ return;
+ end if;
+
+ pragma Assert (Container.First >= 1);
+ pragma Assert (Container.Last >= 1);
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ while Container.Length > 1 loop
+ X := Container.First;
+
+ Container.First := N (X).Next;
+ N (Container.First).Prev := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+
+ X := Container.First;
+
+ Container.First := 0;
+ Container.Last := 0;
+ Container.Length := 0;
+
+ Free (Container, X);
+ end Clear;
+
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : List;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container => Container, Position => Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ return Container.Nodes (Position.Node).Element;
+ end Constant_Reference;
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : List;
+ Item : Element_Type) return Boolean
+ is
+ begin
+ return Find (Container, Item) /= No_Element;
+ end Contains;
+
+ ----------
+ -- Copy --
+ ----------
+
+ function Copy (Source : List) return List
+ is
+ N : Count_Type;
+ P : List;
+
+ begin
+ if Source.Nodes = null then
+ return P;
+ end if;
+
+ P.Nodes := new Node_Array (1 .. Source.Nodes'Length);
+
+ N := 1;
+ while N <= Source.Nodes'Length loop
+ P.Nodes (N).Prev := Source.Nodes (N).Prev;
+ P.Nodes (N).Next := Source.Nodes (N).Next;
+ if Source.Nodes (N).Element /= null then
+ P.Nodes (N).Element :=
+ new Element_Type'(Source.Nodes (N).Element.all);
+ end if;
+ N := N + 1;
+ end loop;
+
+ P.Free := Source.Free;
+ P.Length := Source.Length;
+ P.First := Source.First;
+ P.Last := Source.Last;
+
+ return P;
+ end Copy;
+
+ ------------
+ -- Delete --
+ ------------
+
+ procedure Delete (Container : in out List; Position : in out Cursor) is
+ begin
+ Delete
+ (Container => Container,
+ Position => Position,
+ Count => 1);
+ end Delete;
+
+ procedure Delete
+ (Container : in out List;
+ Position : in out Cursor;
+ Count : Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if not Has_Element (Container => Container,
+ Position => Position)
+ then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Container, Position), "bad cursor in Delete");
+ pragma Assert (Container.First >= 1);
+ pragma Assert (Container.Last >= 1);
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ if Position.Node = Container.First then
+ Delete_First (Container, Count);
+ Position := No_Element;
+ return;
+ end if;
+
+ if Count = 0 then
+ Position := No_Element;
+ return;
+ end if;
+
+ for Index in 1 .. Count loop
+ pragma Assert (Container.Length >= 2);
+
+ X := Position.Node;
+ Container.Length := Container.Length - 1;
+
+ if X = Container.Last then
+ Position := No_Element;
+
+ Container.Last := N (X).Prev;
+ N (Container.Last).Next := 0;
+
+ Free (Container, X);
+ return;
+ end if;
+
+ Position.Node := N (X).Next;
+ pragma Assert (N (Position.Node).Prev >= 0);
+
+ N (N (X).Next).Prev := N (X).Prev;
+ N (N (X).Prev).Next := N (X).Next;
+
+ Free (Container, X);
+ end loop;
+
+ Position := No_Element;
+ end Delete;
+
+ ------------------
+ -- Delete_First --
+ ------------------
+
+ procedure Delete_First (Container : in out List) is
+ begin
+ Delete_First
+ (Container => Container,
+ Count => 1);
+ end Delete_First;
+
+ procedure Delete_First (Container : in out List; Count : Count_Type) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Count >= Container.Length then
+ Clear (Container);
+ return;
+ end if;
+
+ if Count = 0 then
+ return;
+ end if;
+
+ for J in 1 .. Count loop
+ X := Container.First;
+ pragma Assert (N (N (X).Next).Prev = Container.First);
+
+ Container.First := N (X).Next;
+ N (Container.First).Prev := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+ end Delete_First;
+
+ -----------------
+ -- Delete_Last --
+ -----------------
+
+ procedure Delete_Last (Container : in out List) is
+ begin
+ Delete_Last
+ (Container => Container,
+ Count => 1);
+ end Delete_Last;
+
+ procedure Delete_Last (Container : in out List; Count : Count_Type) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Count >= Container.Length then
+ Clear (Container);
+ return;
+ end if;
+
+ if Count = 0 then
+ return;
+ end if;
+
+ for J in 1 .. Count loop
+ X := Container.Last;
+ pragma Assert (N (N (X).Prev).Next = Container.Last);
+
+ Container.Last := N (X).Prev;
+ N (Container.Last).Next := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+ end Delete_Last;
+
+ -------------
+ -- Element --
+ -------------
+
+ function Element
+ (Container : List;
+ Position : Cursor) return Element_Type
+ is
+ begin
+ if not Has_Element (Container => Container, Position => Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ return Container.Nodes (Position.Node).Element.all;
+ end Element;
+
+ ----------------
+ -- Empty_List --
+ ----------------
+
+ function Empty_List return List is
+ ((Controlled with others => <>));
+
+ --------------
+ -- Finalize --
+ --------------
+
+ procedure Finalize (Container : in out List) is
+ X : Count_Type := Container.First;
+ N : Node_Array_Access renames Container.Nodes;
+ begin
+
+ if N = null then
+ return;
+ end if;
+
+ while X /= 0 loop
+ Finalize_Element (N (X).Element);
+ X := N (X).Next;
+ end loop;
+
+ Finalize_Nodes (N);
+
+ Container.Free := 0;
+ Container.Last := 0;
+ Container.First := 0;
+ Container.Length := 0;
+ end Finalize;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ is
+ From : Count_Type := Position.Node;
+
+ begin
+ if From = 0 and Container.Length = 0 then
+ return No_Element;
+ end if;
+
+ if From = 0 then
+ From := Container.First;
+ end if;
+
+ if Position.Node /= 0 and then not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ while From /= 0 loop
+ if Container.Nodes (From).Element.all = Item then
+ return (Node => From);
+ end if;
+
+ From := Container.Nodes (From).Next;
+ end loop;
+
+ return No_Element;
+ end Find;
+
+ -----------
+ -- First --
+ -----------
+
+ function First (Container : List) return Cursor is
+ begin
+ if Container.First = 0 then
+ return No_Element;
+ end if;
+
+ return (Node => Container.First);
+ end First;
+
+ -------------------
+ -- First_Element --
+ -------------------
+
+ function First_Element (Container : List) return Element_Type is
+ F : constant Count_Type := Container.First;
+ begin
+ if F = 0 then
+ raise Constraint_Error with "list is empty";
+ else
+ return Container.Nodes (F).Element.all;
+ end if;
+ end First_Element;
+
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
+
+ procedure Lift_Abstraction_Level (Container : List) is null;
+
+ -------------------------
+ -- M_Elements_In_Union --
+ -------------------------
+
+ function M_Elements_In_Union
+ (Container : M.Sequence;
+ Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
+ Elem : Element_Type;
+
+ begin
+ for Index in 1 .. M.Length (Container) loop
+ Elem := Element (Container, Index);
+
+ if not M.Contains (Left, 1, M.Length (Left), Elem)
+ and then not M.Contains (Right, 1, M.Length (Right), Elem)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_In_Union;
+
+ -------------------------
+ -- M_Elements_Included --
+ -------------------------
+
+ 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
+ is
+ begin
+ for I in L_Fst .. L_Lst loop
+ declare
+ Found : Boolean := False;
+ J : Count_Type := R_Fst - 1;
+
+ begin
+ while not Found and J < R_Lst loop
+ J := J + 1;
+ if Element (Left, I) = Element (Right, J) then
+ Found := True;
+ end if;
+ end loop;
+
+ if not Found then
+ return False;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end M_Elements_Included;
+
+ -------------------------
+ -- M_Elements_Reversed --
+ -------------------------
+
+ function M_Elements_Reversed
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
+ L : constant Count_Type := M.Length (Left);
+
+ begin
+ if L /= M.Length (Right) then
+ return False;
+ end if;
+
+ for I in 1 .. L loop
+ if Element (Left, I) /= Element (Right, L - I + 1) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_Reversed;
+
+ ------------------------
+ -- M_Elements_Swapped --
+ ------------------------
+
+ function M_Elements_Swapped
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ X : Positive_Count_Type;
+ Y : Positive_Count_Type) return Boolean
+ is
+ begin
+ if M.Length (Left) /= M.Length (Right)
+ or else Element (Left, X) /= Element (Right, Y)
+ or else Element (Left, Y) /= Element (Right, X)
+ then
+ return False;
+ end if;
+
+ for I in 1 .. M.Length (Left) loop
+ if I /= X and then I /= Y
+ and then Element (Left, I) /= Element (Right, I)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_Swapped;
+
+ -----------
+ -- Model --
+ -----------
+
+ function Model (Container : List) return M.Sequence is
+ Position : Count_Type := Container.First;
+ R : M.Sequence;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := M.Add (R, Container.Nodes (Position).Element.all);
+ Position := Container.Nodes (Position).Next;
+ end loop;
+
+ return R;
+ end Model;
+
+ -----------------------
+ -- Mapping_Preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (M_Left : M.Sequence;
+ M_Right : M.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > M.Length (M_Left)
+ or else P.Get (P_Right, C) > M.Length (M_Right)
+ or else M.Get (M_Left, P.Get (P_Left, C)) /=
+ M.Get (M_Right, P.Get (P_Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ for C of P_Right loop
+ if not P.Has_Key (P_Left, C) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved;
+
+ -------------------------
+ -- P_Positions_Shifted --
+ -------------------------
+
+ function P_Positions_Shifted
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ is
+ begin
+ for Cu of Small loop
+ if not P.Has_Key (Big, Cu) then
+ return False;
+ end if;
+ end loop;
+
+ for Cu of Big loop
+ declare
+ Pos : constant Positive_Count_Type := P.Get (Big, Cu);
+
+ begin
+ if Pos < Cut then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+
+ elsif Pos >= Cut + Count then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu) + Count
+ then
+ return False;
+ end if;
+
+ else
+ if P.Has_Key (Small, Cu) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end P_Positions_Shifted;
+
+ -------------------------
+ -- P_Positions_Swapped --
+ -------------------------
+
+ function P_Positions_Swapped
+ (Left : P.Map;
+ Right : P.Map;
+ X : Cursor;
+ Y : Cursor) return Boolean
+ is
+ begin
+ if not P.Has_Key (Left, X)
+ or not P.Has_Key (Left, Y)
+ or not P.Has_Key (Right, X)
+ or not P.Has_Key (Right, Y)
+ then
+ return False;
+ end if;
+
+ if P.Get (Left, X) /= P.Get (Right, Y)
+ or P.Get (Left, Y) /= P.Get (Right, X)
+ then
+ return False;
+ end if;
+
+ for C of Left loop
+ if not P.Has_Key (Right, C) then
+ return False;
+ end if;
+ end loop;
+
+ for C of Right loop
+ if not P.Has_Key (Left, C)
+ or else (C /= X
+ and C /= Y
+ and P.Get (Left, C) /= P.Get (Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end P_Positions_Swapped;
+
+ ---------------------------
+ -- P_Positions_Truncated --
+ ---------------------------
+
+ function P_Positions_Truncated
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ is
+ begin
+ for Cu of Small loop
+ if not P.Has_Key (Big, Cu) then
+ return False;
+ end if;
+ end loop;
+
+ for Cu of Big loop
+ declare
+ Pos : constant Positive_Count_Type := P.Get (Big, Cu);
+
+ begin
+ if Pos < Cut then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+
+ elsif Pos >= Cut + Count then
+ return False;
+
+ elsif P.Has_Key (Small, Cu) then
+ return False;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end P_Positions_Truncated;
+
+ ---------------
+ -- Positions --
+ ---------------
+
+ function Positions (Container : List) return P.Map is
+ I : Count_Type := 1;
+ Position : Count_Type := Container.First;
+ R : P.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := P.Add (R, (Node => Position), I);
+ pragma Assert (P.Length (R) = To_Big_Integer (I));
+ Position := Container.Nodes (Position).Next;
+ I := I + 1;
+ end loop;
+
+ return R;
+ end Positions;
+
+ end Formal_Model;
+
+ ----------
+ -- Free --
+ ----------
+
+ procedure Free (Container : in out List; X : Count_Type) is
+ pragma Assert (X > 0);
+ pragma Assert (X <= Container.Nodes'Length);
+
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ N (X).Prev := -1; -- Node is deallocated (not on active list)
+
+ if N (X).Element /= null then
+ Finalize_Element (N (X).Element);
+ end if;
+
+ if Container.Free >= 0 then
+ N (X).Next := Container.Free;
+ Container.Free := X;
+ elsif X + 1 = abs Container.Free then
+ N (X).Next := 0; -- Not strictly necessary, but marginally safer
+ Container.Free := Container.Free + 1;
+ else
+ Container.Free := abs Container.Free;
+
+ for J in Container.Free .. Container.Nodes'Length loop
+ N (J).Next := J + 1;
+ end loop;
+
+ N (Container.Nodes'Length).Next := 0;
+
+ N (X).Next := Container.Free;
+ Container.Free := X;
+ end if;
+ end Free;
+
+ ---------------------
+ -- Generic_Sorting --
+ ---------------------
+
+ package body Generic_Sorting with SPARK_Mode => Off is
+
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
+ begin
+ if M.Length (Container) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (Container, 1);
+
+ begin
+ for I in 2 .. M.Length (Container) loop
+ declare
+ E2 : constant Element_Type := Element (Container, I);
+
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+
+ E1 := E2;
+ end;
+ end loop;
+ end;
+
+ return True;
+ end M_Elements_Sorted;
+
+ end Formal_Model;
+
+ ---------------
+ -- Is_Sorted --
+ ---------------
+
+ function Is_Sorted (Container : List) return Boolean is
+ Nodes : Node_Array_Access renames Container.Nodes;
+ Node : Count_Type := Container.First;
+
+ begin
+ for J in 2 .. Container.Length loop
+ if Nodes (Nodes (Node).Next).Element.all < Nodes (Node).Element.all
+ then
+ return False;
+ else
+ Node := Nodes (Node).Next;
+ end if;
+ end loop;
+
+ return True;
+ end Is_Sorted;
+
+ -----------
+ -- Merge --
+ -----------
+
+ procedure Merge (Target : in out List; Source : in out List) is
+ LN : Node_Array_Access renames Target.Nodes;
+ RN : Node_Array_Access renames Source.Nodes;
+ LI : Cursor;
+ RI : Cursor;
+
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ LI := First (Target);
+ RI := First (Source);
+ while RI.Node /= 0 loop
+ pragma Assert
+ (RN (RI.Node).Next = 0
+ or else not (RN (RN (RI.Node).Next).Element.all <
+ RN (RI.Node).Element.all));
+
+ if LI.Node = 0 then
+ Splice (Target, No_Element, Source);
+ return;
+ end if;
+
+ pragma Assert
+ (LN (LI.Node).Next = 0
+ or else not (LN (LN (LI.Node).Next).Element.all <
+ LN (LI.Node).Element.all));
+
+ if RN (RI.Node).Element.all < LN (LI.Node).Element.all then
+ declare
+ RJ : Cursor := RI;
+ pragma Warnings (Off, RJ);
+ begin
+ RI.Node := RN (RI.Node).Next;
+ Splice (Target, LI, Source, RJ);
+ end;
+
+ else
+ LI.Node := LN (LI.Node).Next;
+ end if;
+ end loop;
+ end Merge;
+
+ ----------
+ -- Sort --
+ ----------
+
+ procedure Sort (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ begin
+ if Container.Length <= 1 then
+ return;
+ end if;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ declare
+ package Descriptors is new List_Descriptors
+ (Node_Ref => Count_Type, Nil => 0);
+ use Descriptors;
+
+ function Next (Idx : Count_Type) return Count_Type is
+ (N (Idx).Next);
+ procedure Set_Next (Idx : Count_Type; Next : Count_Type)
+ with Inline;
+ procedure Set_Prev (Idx : Count_Type; Prev : Count_Type)
+ with Inline;
+ function "<" (L, R : Count_Type) return Boolean is
+ (N (L).Element.all < N (R).Element.all);
+ procedure Update_Container (List : List_Descriptor) with Inline;
+
+ procedure Set_Next (Idx : Count_Type; Next : Count_Type) is
+ begin
+ N (Idx).Next := Next;
+ end Set_Next;
+
+ procedure Set_Prev (Idx : Count_Type; Prev : Count_Type) is
+ begin
+ N (Idx).Prev := Prev;
+ end Set_Prev;
+
+ procedure Update_Container (List : List_Descriptor) is
+ begin
+ Container.First := List.First;
+ Container.Last := List.Last;
+ Container.Length := List.Length;
+ end Update_Container;
+
+ procedure Sort_List is new Doubly_Linked_List_Sort;
+ begin
+ Sort_List (List_Descriptor'(First => Container.First,
+ Last => Container.Last,
+ Length => Container.Length));
+ end;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Sort;
+
+ end Generic_Sorting;
+
+ -----------------
+ -- Has_Element --
+ -----------------
+
+ function Has_Element (Container : List; Position : Cursor) return Boolean is
+ begin
+ if Position.Node = 0 then
+ return False;
+ end if;
+
+ return Container.Nodes (Position.Node).Prev /= -1;
+ end Has_Element;
+
+ ------------
+ -- Insert --
+ ------------
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor;
+ Count : Count_Type)
+ is
+ J : Count_Type;
+
+ begin
+ if Before.Node /= 0 then
+ pragma Assert (Vet (Container, Before), "bad cursor in Insert");
+ end if;
+
+ if Count = 0 then
+ Position := Before;
+ return;
+ end if;
+ Allocate (Container, New_Item, New_Node => J);
+ Insert_Internal (Container, Before.Node, New_Node => J);
+ Position := (Node => J);
+
+ for Index in 2 .. Count loop
+ Allocate (Container, New_Item, New_Node => J);
+ Insert_Internal (Container, Before.Node, New_Node => J);
+ end loop;
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor)
+ is
+ begin
+ Insert
+ (Container => Container,
+ Before => Before,
+ New_Item => New_Item,
+ Position => Position,
+ Count => 1);
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ Position : Cursor;
+
+ begin
+ Insert (Container, Before, New_Item, Position, Count);
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type)
+ is
+ Position : Cursor;
+
+ begin
+ Insert (Container, Before, New_Item, Position, 1);
+ end Insert;
+
+ ---------------------
+ -- Insert_Internal --
+ ---------------------
+
+ procedure Insert_Internal
+ (Container : in out List;
+ Before : Count_Type;
+ New_Node : Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Container.Length = 0 then
+ pragma Assert (Before = 0);
+ pragma Assert (Container.First = 0);
+ pragma Assert (Container.Last = 0);
+
+ Container.First := New_Node;
+ Container.Last := New_Node;
+
+ N (Container.First).Prev := 0;
+ N (Container.Last).Next := 0;
+
+ elsif Before = 0 then
+ pragma Assert (N (Container.Last).Next = 0);
+
+ N (Container.Last).Next := New_Node;
+ N (New_Node).Prev := Container.Last;
+
+ Container.Last := New_Node;
+ N (Container.Last).Next := 0;
+
+ elsif Before = Container.First then
+ pragma Assert (N (Container.First).Prev = 0);
+
+ N (Container.First).Prev := New_Node;
+ N (New_Node).Next := Container.First;
+
+ Container.First := New_Node;
+ N (Container.First).Prev := 0;
+
+ else
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ N (New_Node).Next := Before;
+ N (New_Node).Prev := N (Before).Prev;
+
+ N (N (Before).Prev).Next := New_Node;
+ N (Before).Prev := New_Node;
+ end if;
+ Container.Length := Container.Length + 1;
+ end Insert_Internal;
+
+ --------------
+ -- Is_Empty --
+ --------------
+
+ function Is_Empty (Container : List) return Boolean is
+ begin
+ return Length (Container) = 0;
+ end Is_Empty;
+
+ ----------
+ -- Last --
+ ----------
+
+ function Last (Container : List) return Cursor is
+ begin
+ if Container.Last = 0 then
+ return No_Element;
+ end if;
+
+ return (Node => Container.Last);
+ end Last;
+
+ ------------------
+ -- Last_Element --
+ ------------------
+
+ function Last_Element (Container : List) return Element_Type is
+ L : constant Count_Type := Container.Last;
+
+ begin
+ if L = 0 then
+ raise Constraint_Error with "list is empty";
+ else
+ return Container.Nodes (L).Element.all;
+ end if;
+ end Last_Element;
+
+ ------------
+ -- Length --
+ ------------
+
+ function Length (Container : List) return Count_Type is
+ begin
+ return Container.Length;
+ end Length;
+
+ ----------
+ -- Move --
+ ----------
+
+ procedure Move (Target : in out List; Source : in out List) is
+ N : Node_Array_Access renames Source.Nodes;
+
+ procedure Finalize_Node_Array is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ begin
+ if Target'Address = Source'Address then
+ return;
+ end if;
+
+ Clear (Target);
+
+ if Source.Length = 0 then
+ return;
+ end if;
+
+ -- Make sure that Target is large enough
+
+ if Target.Nodes = null
+ or else Target.Nodes'Length < Source.Length
+ then
+ if Target.Nodes /= null then
+ Finalize_Node_Array (Target.Nodes);
+ end if;
+ Target.Nodes := new Node_Array (1 .. Source.Length);
+ end if;
+
+ -- Copy first element from Source to Target
+
+ Target.First := 1;
+
+ Target.Nodes (1).Prev := 0;
+ Target.Nodes (1).Element := N (Source.First).Element;
+ N (Source.First).Element := null;
+
+ -- Copy the other elements
+
+ declare
+ X_Src : Count_Type := N (Source.First).Next;
+ X_Tar : Count_Type := 2;
+
+ begin
+ while X_Src /= 0 loop
+ Target.Nodes (X_Tar).Prev := X_Tar - 1;
+ Target.Nodes (X_Tar - 1).Next := X_Tar;
+
+ Target.Nodes (X_Tar).Element := N (X_Src).Element;
+ N (X_Src).Element := null;
+
+ X_Src := N (X_Src).Next;
+ X_Tar := X_Tar + 1;
+ end loop;
+ end;
+
+ Target.Last := Source.Length;
+ Target.Length := Source.Length;
+ Target.Nodes (Target.Last).Next := 0;
+
+ -- Set up the free list
+
+ Target.Free := -Source.Length - 1;
+
+ -- It is possible to Clear Source because the Element accesses were
+ -- set to null.
+
+ Clear (Source);
+ end Move;
+
+ ----------
+ -- Next --
+ ----------
+
+ procedure Next (Container : List; Position : in out Cursor) is
+ begin
+ Position := Next (Container, Position);
+ end Next;
+
+ function Next (Container : List; Position : Cursor) return Cursor is
+ begin
+ if Position.Node = 0 then
+ return No_Element;
+ end if;
+
+ if not Has_Element (Container, Position) then
+ raise Program_Error with "Position cursor has no element";
+ end if;
+
+ return (Node => Container.Nodes (Position.Node).Next);
+ end Next;
+
+ -------------
+ -- Prepend --
+ -------------
+
+ procedure Prepend (Container : in out List; New_Item : Element_Type) is
+ begin
+ Insert (Container, First (Container), New_Item, 1);
+ end Prepend;
+
+ procedure Prepend
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ begin
+ Insert (Container, First (Container), New_Item, Count);
+ end Prepend;
+
+ --------------
+ -- Previous --
+ --------------
+
+ procedure Previous (Container : List; Position : in out Cursor) is
+ begin
+ Position := Previous (Container, Position);
+ end Previous;
+
+ function Previous (Container : List; Position : Cursor) return Cursor is
+ begin
+ if Position.Node = 0 then
+ return No_Element;
+ end if;
+
+ if not Has_Element (Container, Position) then
+ raise Program_Error with "Position cursor has no element";
+ end if;
+
+ return (Node => Container.Nodes (Position.Node).Prev);
+ end Previous;
+
+ ---------------
+ -- Reference --
+ ---------------
+
+ function Reference
+ (Container : not null access List;
+ Position : Cursor) return not null access Element_Type
+ is
+ begin
+ if not Has_Element (Container.all, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ return Container.Nodes (Position.Node).Element;
+ end Reference;
+
+ ---------------------
+ -- Replace_Element --
+ ---------------------
+
+ procedure Replace_Element
+ (Container : in out List;
+ Position : Cursor;
+ New_Item : Element_Type)
+ is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position), "bad cursor in Replace_Element");
+
+ Finalize_Element (Container.Nodes (Position.Node).Element);
+ Container.Nodes (Position.Node).Element := new Element_Type'(New_Item);
+ end Replace_Element;
+
+ ------------
+ -- Resize --
+ ------------
+
+ procedure Resize (Container : in out List) is
+ Min_Size : constant Count_Type := 100;
+ begin
+ if Container.Nodes = null then
+ Container.Nodes := new Node_Array (1 .. Min_Size);
+ Container.First := 0;
+ Container.Last := 0;
+ Container.Length := 0;
+ Container.Free := -1;
+
+ return;
+ end if;
+
+ if Container.Length /= Container.Nodes'Length then
+ raise Program_Error with "List must be at size max to resize";
+ end if;
+
+ declare
+ procedure Finalize_Node_Array is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ New_Size : constant Count_Type :=
+ (if Container.Nodes'Length > Count_Type'Last / 2
+ then Count_Type'Last
+ else 2 * Container.Nodes'Length);
+ New_Nodes : Node_Array_Access;
+
+ begin
+ New_Nodes :=
+ new Node_Array (1 .. Count_Type'Max (New_Size, Min_Size));
+
+ New_Nodes (1 .. Container.Nodes'Length) :=
+ Container.Nodes (1 .. Container.Nodes'Length);
+
+ Container.Free := -Container.Nodes'Length - 1;
+
+ Finalize_Node_Array (Container.Nodes);
+ Container.Nodes := New_Nodes;
+ end;
+ end Resize;
+
+ ----------------------
+ -- Reverse_Elements --
+ ----------------------
+
+ procedure Reverse_Elements (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ I : Count_Type := Container.First;
+ J : Count_Type := Container.Last;
+
+ procedure Swap (L : Count_Type; R : Count_Type);
+
+ ----------
+ -- Swap --
+ ----------
+
+ procedure Swap (L : Count_Type; R : Count_Type) is
+ LN : constant Count_Type := N (L).Next;
+ LP : constant Count_Type := N (L).Prev;
+
+ RN : constant Count_Type := N (R).Next;
+ RP : constant Count_Type := N (R).Prev;
+
+ begin
+ if LP /= 0 then
+ N (LP).Next := R;
+ end if;
+
+ if RN /= 0 then
+ N (RN).Prev := L;
+ end if;
+
+ N (L).Next := RN;
+ N (R).Prev := LP;
+
+ if LN = R then
+ pragma Assert (RP = L);
+
+ N (L).Prev := R;
+ N (R).Next := L;
+
+ else
+ N (L).Prev := RP;
+ N (RP).Next := L;
+
+ N (R).Next := LN;
+ N (LN).Prev := R;
+ end if;
+ end Swap;
+
+ -- Start of processing for Reverse_Elements
+
+ begin
+ if Container.Length <= 1 then
+ return;
+ end if;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ Container.First := J;
+ Container.Last := I;
+ loop
+ Swap (L => I, R => J);
+
+ J := N (J).Next;
+ exit when I = J;
+
+ I := N (I).Prev;
+ exit when I = J;
+
+ Swap (L => J, R => I);
+
+ I := N (I).Next;
+ exit when I = J;
+
+ J := N (J).Prev;
+ exit when I = J;
+ end loop;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Reverse_Elements;
+
+ ------------------
+ -- Reverse_Find --
+ ------------------
+
+ function Reverse_Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ is
+ CFirst : Count_Type := Position.Node;
+
+ begin
+ if CFirst = 0 then
+ CFirst := Container.Last;
+ end if;
+
+ if Container.Length = 0 then
+ return No_Element;
+ else
+ while CFirst /= 0 loop
+ if Container.Nodes (CFirst).Element.all = Item then
+ return (Node => CFirst);
+ else
+ CFirst := Container.Nodes (CFirst).Prev;
+ end if;
+ end loop;
+
+ return No_Element;
+ end if;
+ end Reverse_Find;
+
+ ------------
+ -- Splice --
+ ------------
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List)
+ is
+ SN : Node_Array_Access renames Source.Nodes;
+ TN : Node_Array_Access renames Target.Nodes;
+
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ if Before.Node /= 0 then
+ pragma Assert (Vet (Target, Before), "bad cursor in Splice");
+ end if;
+
+ if Is_Empty (Source) then
+ return;
+ end if;
+
+ pragma Assert (SN (Source.First).Prev = 0);
+ pragma Assert (SN (Source.Last).Next = 0);
+
+ declare
+ X : Count_Type;
+
+ begin
+ while not Is_Empty (Source) loop
+ Allocate (Target, X);
+
+ TN (X).Element := SN (Source.Last).Element;
+
+ -- Insert the new node in Target
+
+ Insert_Internal (Target, Before.Node, X);
+
+ -- Free the last node of Source
+
+ SN (Source.Last).Element := null;
+ Delete_Last (Source);
+ end loop;
+ end;
+
+ end Splice;
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List;
+ Position : in out Cursor)
+ is
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ if Position.Node = 0 then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Source, Position), "bad Position cursor in Splice");
+
+ declare
+ X : Count_Type;
+
+ begin
+ Allocate (Target, X);
+
+ Target.Nodes (X).Element := Source.Nodes (Position.Node).Element;
+
+ -- Insert the new node in Target
+
+ Insert_Internal (Target, Before.Node, X);
+
+ -- Free the node at position Position in Source
+
+ Source.Nodes (Position.Node).Element := null;
+ Delete (Source, Position);
+
+ Position := (Node => X);
+ end;
+ end Splice;
+
+ procedure Splice
+ (Container : in out List;
+ Before : Cursor;
+ Position : Cursor)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Before.Node /= 0 then
+ pragma Assert
+ (Vet (Container, Before), "bad Before cursor in Splice");
+ end if;
+
+ if Position.Node = 0 then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position), "bad Position cursor in Splice");
+
+ if Position.Node = Before.Node
+ or else N (Position.Node).Next = Before.Node
+ then
+ return;
+ end if;
+
+ pragma Assert (Container.Length >= 2);
+
+ if Before.Node = 0 then
+ pragma Assert (Position.Node /= Container.Last);
+
+ if Position.Node = Container.First then
+ Container.First := N (Position.Node).Next;
+ N (Container.First).Prev := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (Container.Last).Next := Position.Node;
+ N (Position.Node).Prev := Container.Last;
+
+ Container.Last := Position.Node;
+ N (Container.Last).Next := 0;
+
+ return;
+ end if;
+
+ if Before.Node = Container.First then
+ pragma Assert (Position.Node /= Container.First);
+
+ if Position.Node = Container.Last then
+ Container.Last := N (Position.Node).Prev;
+ N (Container.Last).Next := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (Container.First).Prev := Position.Node;
+ N (Position.Node).Next := Container.First;
+
+ Container.First := Position.Node;
+ N (Container.First).Prev := 0;
+
+ return;
+ end if;
+
+ if Position.Node = Container.First then
+ Container.First := N (Position.Node).Next;
+ N (Container.First).Prev := 0;
+
+ elsif Position.Node = Container.Last then
+ Container.Last := N (Position.Node).Prev;
+ N (Container.Last).Next := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (N (Before.Node).Prev).Next := Position.Node;
+ N (Position.Node).Prev := N (Before.Node).Prev;
+
+ N (Before.Node).Prev := Position.Node;
+ N (Position.Node).Next := Before.Node;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Splice;
+
+ ----------
+ -- Swap --
+ ----------
+
+ procedure Swap
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ is
+ begin
+ if I.Node = 0 then
+ raise Constraint_Error with "I cursor has no element";
+ end if;
+
+ if J.Node = 0 then
+ raise Constraint_Error with "J cursor has no element";
+ end if;
+
+ if I.Node = J.Node then
+ return;
+ end if;
+
+ pragma Assert (Vet (Container, I), "bad I cursor in Swap");
+ pragma Assert (Vet (Container, J), "bad J cursor in Swap");
+
+ declare
+ NN : Node_Array_Access renames Container.Nodes;
+ NI : Node_Type renames NN (I.Node);
+ NJ : Node_Type renames NN (J.Node);
+
+ EI_Copy : constant Element_Access := NI.Element;
+
+ begin
+ NI.Element := NJ.Element;
+ NJ.Element := EI_Copy;
+ end;
+ end Swap;
+
+ ----------------
+ -- Swap_Links --
+ ----------------
+
+ procedure Swap_Links
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ is
+ I_Next : Cursor;
+ J_Next : Cursor;
+
+ begin
+ if I.Node = 0 then
+ raise Constraint_Error with "I cursor has no element";
+ end if;
+
+ if J.Node = 0 then
+ raise Constraint_Error with "J cursor has no element";
+ end if;
+
+ if I.Node = J.Node then
+ return;
+ end if;
+
+ pragma Assert (Vet (Container, I), "bad I cursor in Swap_Links");
+ pragma Assert (Vet (Container, J), "bad J cursor in Swap_Links");
+
+ I_Next := Next (Container, I);
+
+ if I_Next = J then
+ Splice (Container, Before => I, Position => J);
+
+ else
+ J_Next := Next (Container, J);
+
+ if J_Next = I then
+ Splice (Container, Before => J, Position => I);
+
+ else
+ pragma Assert (Container.Length >= 3);
+ Splice (Container, Before => I_Next, Position => J);
+ Splice (Container, Before => J_Next, Position => I);
+ end if;
+ end if;
+ end Swap_Links;
+
+ ---------
+ -- Vet --
+ ---------
+
+ function Vet (L : List; Position : Cursor) return Boolean is
+ N : Node_Array_Access renames L.Nodes;
+ begin
+ if not Container_Checks'Enabled then
+ return True;
+ end if;
+
+ if L.Length = 0 then
+ return False;
+ end if;
+
+ if L.First = 0 then
+ return False;
+ end if;
+
+ if L.Last = 0 then
+ return False;
+ end if;
+
+ if Position.Node > L.Nodes'Length then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev < 0
+ or else N (Position.Node).Prev > L.Nodes'Length
+ then
+ return False;
+ end if;
+
+ if N (Position.Node).Next > L.Nodes'Length then
+ return False;
+ end if;
+
+ if N (L.First).Prev /= 0 then
+ return False;
+ end if;
+
+ if N (L.Last).Next /= 0 then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
+ return False;
+ end if;
+
+ if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 1 then
+ return L.First = L.Last;
+ end if;
+
+ if L.First = L.Last then
+ return False;
+ end if;
+
+ if N (L.First).Next = 0 then
+ return False;
+ end if;
+
+ if N (L.Last).Prev = 0 then
+ return False;
+ end if;
+
+ if N (N (L.First).Next).Prev /= L.First then
+ return False;
+ end if;
+
+ if N (N (L.Last).Prev).Next /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 2 then
+ if N (L.First).Next /= L.Last then
+ return False;
+ end if;
+
+ if N (L.Last).Prev /= L.First then
+ return False;
+ end if;
+
+ return True;
+ end if;
+
+ if N (L.First).Next = L.Last then
+ return False;
+ end if;
+
+ if N (L.Last).Prev = L.First then
+ return False;
+ end if;
+
+ if Position.Node = L.First then
+ return True;
+ end if;
+
+ if Position.Node = L.Last then
+ return True;
+ end if;
+
+ if N (Position.Node).Next = 0 then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev = 0 then
+ return False;
+ end if;
+
+ if N (N (Position.Node).Next).Prev /= Position.Node then
+ return False;
+ end if;
+
+ if N (N (Position.Node).Prev).Next /= Position.Node then
+ return False;
+ end if;
+
+ if L.Length = 3 then
+ if N (L.First).Next /= Position.Node then
+ return False;
+ end if;
+
+ if N (L.Last).Prev /= Position.Node then
+ return False;
+ end if;
+ end if;
+
+ return True;
+ end Vet;
+
+end Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_DOUBLY_LINKED_LISTS --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022-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;
+private with Ada.Finalization;
+
+generic
+ type Element_Type is private;
+ with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Indefinite_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 is private with
+ Iterable => (First => First,
+ Next => Next,
+ Has_Element => Has_Element,
+ Element => Element),
+ Default_Initial_Condition => Is_Empty (List);
+
+ type Cursor is record
+ Node : Count_Type := 0;
+ end record;
+
+ No_Element : constant Cursor := Cursor'(Node => 0);
+
+ function Length (Container : List) return Count_Type with
+ Global => null;
+
+ function Empty_List return List with
+ Global => null,
+ Post => Length (Empty_List'Result) = 0;
+
+ 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,
+ Post => Model (Target) = Model (Source);
+
+ function Copy (Source : List) return List with
+ Global => null,
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Positions (Copy'Result) = Positions (Source);
+
+ 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 : 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,
+ 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) < Count_Type'Last
+ 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) <= Count_Type'Last - 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))
+
+ -- 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) < Count_Type'Last
+ 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) <= Count_Type'Last - 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) < Count_Type'Last,
+ 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) <= Count_Type'Last - 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) < Count_Type'Last,
+ 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) <= Count_Type'Last - 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) <= Count_Type'Last - 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) < Count_Type'Last,
+ 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 (Target) <= Count_Type'Last - Length (Source),
+ 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);
+
+ use Ada.Finalization;
+
+ type Element_Access is access all Element_Type;
+
+ type Node_Type is record
+ Prev : Count_Type'Base := -1;
+ Next : Count_Type := 0;
+ Element : Element_Access := null;
+ end record;
+
+ type Node_Access is access all Node_Type;
+
+ 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 Node_Array_Access is access all Node_Array;
+
+ type List is new Controlled with record
+ Free : Count_Type'Base := -1;
+ Length : Count_Type := 0;
+ First : Count_Type := 0;
+ Last : Count_Type := 0;
+ Nodes : Node_Array_Access := null;
+ end record;
+
+ overriding procedure Finalize (Container : in out List);
+ overriding procedure Adjust (Container : in out List);
+end Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists;
projects / thirdparty / gcc.git / commitdiff
