[Ada] Provide extended contracts for formal doubly linked lists
Arnaud Charlet
charlet@adacore.com
Thu Apr 27 09:57:00 GMT 2017
Primitives of doubly linked lists are now annotated with precise
contracts which can be used for formal verification with GNATprove.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-04-27 Claire Dross <dross@adacore.com>
* a-cfdlli.adb, a-cfdlli.ads (=): Generic parameter removed to
allow the use of regular equality over elements in contracts.
(Cursor): Type is now public so that it can be used in
model functions.
(Formal_Model): Ghost package containing
model functions that are used in subprogram contracts.
(Current_To_Last): Removed, model functions should be used
instead.
(First_To_Previous): Removed, model functions should
be used instead.
(Strict_Equal): Removed, model functions
should be used instead.
(Append): Default parameter value
replaced by new wrapper to allow more precise contracts.
(Insert): Default parameter value replaced by new wrapper to
allow more precise contracts.
(Delete): Default parameter
value replaced by new wrapper to allow more precise contracts.
(Prepend): Default parameter value replaced by new wrapper to
allow more precise contracts.
(Delete_First): Default parameter
value replaced by new wrapper to allow more precise contracts.
(Delete_Last): Default parameter value replaced by new wrapper
to allow more precise contracts.
-------------- next part --------------
Index: a-cfdlli.adb
===================================================================
--- a-cfdlli.adb (revision 247293)
+++ a-cfdlli.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
-- --
-- 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- --
@@ -40,10 +40,6 @@
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);
@@ -109,31 +105,22 @@
end if;
end Allocate;
- procedure Allocate
- (Container : in out List;
- New_Node : out Count_Type)
- is
- N : Node_Array renames Container.Nodes;
-
- begin
- 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;
- 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 := 1)
+ Count : Count_Type)
is
begin
Insert (Container, No_Element, New_Item, Count);
@@ -161,7 +148,7 @@
J := Source.First;
while J /= 0 loop
- Append (Target, N (J).Element);
+ Append (Target, N (J).Element, 1);
J := N (J).Next;
end loop;
end Assign;
@@ -259,44 +246,24 @@
return P;
end Copy;
- ---------------------
- -- Current_To_Last --
- ---------------------
-
- function Current_To_Last
- (Container : List;
- Current : Cursor) return List is
- Curs : Cursor := First (Container);
- C : List (Container.Capacity) := Copy (Container, Container.Capacity);
- Node : Count_Type;
-
- begin
- if Curs = No_Element then
- Clear (C);
- return C;
- end if;
-
- if Current /= No_Element and not Has_Element (Container, Current) then
- raise Constraint_Error;
- end if;
-
- while Curs.Node /= Current.Node loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
- end loop;
-
- return C;
- end Current_To_Last;
-
------------
-- 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 := 1)
+ Count : Count_Type)
is
N : Node_Array renames Container.Nodes;
X : Count_Type;
@@ -357,9 +324,16 @@
-- 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 := 1)
+ Count : Count_Type)
is
N : Node_Array renames Container.Nodes;
X : Count_Type;
@@ -391,9 +365,16 @@
-- 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 := 1)
+ Count : Count_Type)
is
N : Node_Array renames Container.Nodes;
X : Count_Type;
@@ -503,36 +484,356 @@
end if;
end First_Element;
- -----------------------
- -- First_To_Previous --
- -----------------------
+ ------------------
+ -- Formal_Model --
+ ------------------
- function First_To_Previous
- (Container : List;
- Current : Cursor) return List
- is
- Curs : Cursor := Current;
- C : List (Container.Capacity) := Copy (Container, Container.Capacity);
- Node : Count_Type;
+ package body Formal_Model is
- begin
- if Curs = No_Element then
- return C;
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
- elsif not Has_Element (Container, Curs) then
- raise Constraint_Error;
+ procedure Lift_Abstraction_Level (Container : List) is null;
- else
- while Curs.Node /= 0 loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
+ -------------------------
+ -- M_Elements_Contains --
+ -------------------------
+
+ function M_Elements_Contains
+ (S : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ E : Element_Type)
+ return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if Element (S, I) = E then
+ return True;
+ end if;
end loop;
+ return False;
+ end M_Elements_Contains;
- return C;
- end if;
- end First_To_Previous;
+ --------------------
+ -- M_Elements_Cst --
+ --------------------
+ function M_Elements_Cst
+ (S : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ E : Element_Type)
+ return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if Element (S, I) /= E then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end M_Elements_Cst;
+
+ ----------------------
+ -- M_Elements_Equal --
+ ----------------------
+
+ function M_Elements_Equal
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type)
+ return Boolean
+ is
+ begin
+ return M_Elements_Shifted (S1, S2, Fst, Lst, 0);
+ end M_Elements_Equal;
+
+ -------------------------
+ -- M_Elements_Reversed --
+ -------------------------
+
+ function M_Elements_Reversed (S1, S2 : M.Sequence) return Boolean is
+ L : constant Count_Type := M.Length (S1);
+ begin
+ if L /= M.Length (S2) then
+ return False;
+ end if;
+
+ for I in 1 .. L loop
+ if Element (S1, I) /= Element (S2, L - I + 1)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_Reversed;
+
+ ------------------------
+ -- M_Elements_Shifted --
+ ------------------------
+
+ function M_Elements_Shifted
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Offset : Count_Type'Base := 1)
+ return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if Element (S1, I) /= Element (S2, I + Offset) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end M_Elements_Shifted;
+
+ -------------------------
+ -- M_Elements_Shuffled --
+ -------------------------
+
+ function M_Elements_Shuffle
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Offset : Count_Type'Base)
+ return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ declare
+ Found : Boolean := False;
+ J : Count_Type := Fst;
+ begin
+ while not Found and J <= Lst loop
+ if Element (S1, I) = Element (S2, J + Offset) then
+ Found := True;
+ end if;
+ J := J + 1;
+ end loop;
+
+ if not Found then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end M_Elements_Shuffle;
+
+ ------------------------
+ -- M_Elements_Swapted --
+ ------------------------
+
+ function M_Elements_Swapped
+ (S1, S2 : M.Sequence;
+ X, Y : Positive_Count_Type)
+ return Boolean
+ is
+ begin
+ if M.Length (S1) /= M.Length (S2)
+ or else Element (S1, X) /= Element (S2, Y)
+ or else Element (S1, Y) /= Element (S2, X)
+ then
+ return False;
+ end if;
+
+ for I in 1 .. M.Length (S1) loop
+ if I /= X and then I /= Y
+ and then Element (S1, I) /= Element (S2, 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);
+ Position := Container.Nodes (Position).Next;
+ end loop;
+ return R;
+ end Model;
+
+ -----------------------
+ -- Mapping_preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (S1, S2 : M.Sequence;
+ M1, M2 : P.Map) return Boolean is
+
+ begin
+ for C of M1 loop
+ if not P.Mem (M2, C)
+ or else P.Get (M1, C) > M.Length (S1)
+ or else P.Get (M2, C) > M.Length (S2)
+ or else M.Get (S1, P.Get (M1, C)) /= M.Get (S2, P.Get (M2, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ for C of M2 loop
+ if not P.Mem (M1, 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.Mem (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.Mem (Small, Cu) or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+ elsif Pos >= Cut + Count then
+ if not P.Mem (Small, Cu)
+ or else Pos /= P.Get (Small, Cu) + Count
+ then
+ return False;
+ end if;
+ else
+ if P.Mem (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
+ (M1, M2 : P.Map;
+ C1, C2 : Cursor) return Boolean
+ is
+ begin
+ if not P.Mem (M1, C1) or not P.Mem (M1, C2)
+ or not P.Mem (M2, C1) or not P.Mem (M2, C2)
+ then
+ return False;
+ end if;
+
+ if P.Get (M1, C1) /= P.Get (M2, C2)
+ or P.Get (M1, C2) /= P.Get (M2, C1)
+ then
+ return False;
+ end if;
+
+ for C of M1 loop
+ if not P.Mem (M2, C) then
+ return False;
+ end if;
+ end loop;
+
+ for C of M2 loop
+ if not P.Mem (M1, C)
+ or else (C /= C1 and C /= C2 and P.Get (M1, C) /= P.Get (M2, 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.Mem (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.Mem (Small, Cu) or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+ elsif Pos >= Cut + Count then
+ return False;
+ elsif P.Mem (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
+ Position : Count_Type := Container.First;
+ R : P.Map;
+ I : Count_Type := 1;
+ 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) = I);
+ Position := Container.Nodes (Position).Next;
+ I := I + 1;
+ end loop;
+ return R;
+ end Positions;
+
+ end Formal_Model;
+
----------
-- Free --
----------
@@ -602,6 +903,33 @@
return True;
end Is_Sorted;
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (S : M.Sequence) return Boolean is
+ begin
+ if M.Length (S) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (S, 1);
+ begin
+ for I in 2 .. M.Length (S) loop
+ declare
+ E2 : constant Element_Type := Element (S, I);
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+ E1 := E2;
+ end;
+ end loop;
+ end;
+ return True;
+ end M_Elements_Sorted;
+
-----------
-- Merge --
-----------
@@ -766,7 +1094,7 @@
Before : Cursor;
New_Item : Element_Type;
Position : out Cursor;
- Count : Count_Type := 1)
+ Count : Count_Type)
is
J : Count_Type;
@@ -798,8 +1126,22 @@
(Container : in out List;
Before : Cursor;
New_Item : Element_Type;
- Count : Count_Type := 1)
+ 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);
@@ -808,33 +1150,11 @@
procedure Insert
(Container : in out List;
Before : Cursor;
- Position : out Cursor;
- Count : Count_Type := 1)
+ New_Item : Element_Type)
is
- J : Count_Type;
-
+ Position : Cursor;
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;
-
- if Container.Length > Container.Capacity - Count then
- raise Constraint_Error with "new length exceeds capacity";
- end if;
-
- Allocate (Container, New_Node => J);
- Insert_Internal (Container, Before.Node, New_Node => J);
- Position := (Node => J);
-
- for Index in 2 .. Count loop
- Allocate (Container, New_Node => J);
- Insert_Internal (Container, Before.Node, New_Node => J);
- end loop;
+ Insert (Container, Before, New_Item, Position, 1);
end Insert;
---------------------
@@ -1046,8 +1366,16 @@
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 := 1)
+ Count : Count_Type)
is
begin
Insert (Container, First (Container), New_Item, Count);
@@ -1377,29 +1705,6 @@
pragma Assert (N (Container.Last).Next = 0);
end Splice;
- ------------------
- -- Strict_Equal --
- ------------------
-
- function Strict_Equal (Left, Right : List) return Boolean is
- CL : Count_Type := Left.First;
- CR : Count_Type := Right.First;
-
- begin
- while CL /= 0 or CR /= 0 loop
- if CL /= CR or else
- Left.Nodes (CL).Element /= Right.Nodes (CL).Element
- then
- return False;
- end if;
-
- CL := Left.Nodes (CL).Next;
- CR := Right.Nodes (CR).Next;
- end loop;
-
- return True;
- end Strict_Equal;
-
----------
-- Swap --
----------
Index: a-cfdlli.ads
===================================================================
--- a-cfdlli.ads (revision 247293)
+++ a-cfdlli.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2017, 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 --
@@ -29,43 +29,14 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
--- This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists in the
--- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
--- making it easier to express properties, and by making the specification of
--- this unit compatible with SPARK 2014. Note that the API of this unit may be
--- subject to incompatible changes as SPARK 2014 evolves.
+with Ada.Containers.Functional_Vectors;
+with Ada.Containers.Functional_Maps;
--- The modifications are:
-
--- A parameter for the container is added to every function reading the
--- contents of a container: Next, Previous, Query_Element, Has_Element,
--- Iterate, Reverse_Iterate, Element. This change is motivated by the need
--- to have cursors which are valid on different containers (typically a
--- container C and its previous version C'Old) for expressing properties,
--- which is not possible if cursors encapsulate an access to the underlying
--- container.
-
--- There are three new functions:
-
--- function Strict_Equal (Left, Right : List) return Boolean;
--- function First_To_Previous (Container : List; Current : Cursor)
--- return List;
--- function Current_To_Last (Container : List; Current : Cursor)
--- return List;
-
--- See subprogram specifications that follow for details
-
generic
type Element_Type is private;
-
- with function "=" (Left, Right : Element_Type)
- return Boolean is <>;
-
package Ada.Containers.Formal_Doubly_Linked_Lists with
- Pure,
SPARK_Mode
is
- pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis);
type List (Capacity : Count_Type) is private with
@@ -76,39 +47,334 @@
Default_Initial_Condition => Is_Empty (List);
pragma Preelaborable_Initialization (List);
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
+ type Cursor is record
+ Node : Count_Type := 0;
+ end record;
+ No_Element : constant Cursor := Cursor'(Node => 0);
+
Empty_List : constant List;
- No_Element : constant Cursor;
+ 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, Right : M.Sequence) return Boolean renames M."=";
+ function "<" (Left, Right : M.Sequence) return Boolean renames M."<";
+ function "<=" (Left, Right : M.Sequence) return Boolean renames M."<=";
+
+ function M_Elements_Contains
+ (S : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ E : Element_Type)
+ return Boolean
+ -- E appears in the slice from Fst to Lst in S
+ with
+ Global => null,
+ Pre => Lst <= M.Length (S),
+ Post =>
+ M_Elements_Contains'Result =
+ (for some I in Fst .. Lst => Element (S, I) = E);
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Contains);
+
+ function M_Elements_Cst
+ (S : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ E : Element_Type)
+ return Boolean
+ -- Every element of the slice from Fst to Lst in S is E.
+ with
+ Global => null,
+ Pre => Lst <= M.Length (S),
+ Post =>
+ M_Elements_Cst'Result =
+ (for all I in Fst .. Lst => Element (S, I) = E);
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Cst);
+
+ function M_Elements_Equal
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type)
+ return Boolean
+ -- The slice from Fst to Lst is the same in S1 and S2
+ with
+ Global => null,
+ Pre => Lst <= M.Length (S1) and Lst <= M.Length (S2),
+ Post =>
+ M_Elements_Equal'Result =
+ (for all I in Fst .. Lst => Element (S1, I) = Element (S2, I));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Equal);
+
+ function M_Elements_Shuffle
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Offset : Count_Type'Base)
+ return Boolean
+ -- The slice from Fst to Lst in S1 contains the same elements than the
+ -- same slide shifted by Offset in S2
+ with
+ Global => null,
+ Pre =>
+ Lst <= M.Length (S1)
+ and Offset in 1 - Fst .. M.Length (S2) - Lst,
+ Post =>
+ M_Elements_Shuffle'Result =
+ (for all J in Fst + Offset .. Lst + Offset =>
+ (for some I in Fst .. Lst =>
+ Element (S1, I) = Element (S2, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shuffle);
+
+ function M_Elements_Reversed (S1, S2 : M.Sequence) return Boolean
+ -- S2 is S1 in reverse order
+ with
+ Global => null,
+ Post =>
+ M_Elements_Reversed'Result =
+ (M.Length (S1) = M.Length (S2)
+ and (for all I in 1 .. M.Length (S1) =>
+ Element (S1, I) = Element (S2, M.Length (S1) - I + 1))
+ and (for all I in 1 .. M.Length (S1) =>
+ Element (S2, I) = Element (S1, M.Length (S1) - I + 1)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
+
+ function M_Elements_Shifted
+ (S1, S2 : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Offset : Count_Type'Base := 1)
+ return Boolean
+ -- The slice from Fst to Lst in S1 has been shifted by Offset in S2.
+ with
+ Global => null,
+ Pre =>
+ Lst <= M.Length (S1)
+ and Offset in 1 - Fst .. M.Length (S2) - Lst,
+ Post =>
+ M_Elements_Shifted'Result =
+ ((for all I in Fst .. Lst =>
+ Element (S1, I) = Element (S2, I + Offset))
+ and (for all I in Fst + Offset .. Lst + Offset =>
+ Element (S1, I - Offset) = Element (S2, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shifted);
+
+ function M_Elements_Swapped
+ (S1, S2 : M.Sequence;
+ X, Y : Positive_Count_Type)
+ return Boolean
+ -- Elements stored at X and Y are reversed in S1 and S2
+ with
+ Global => null,
+ Pre => X <= M.Length (S1) and Y <= M.Length (S1),
+ Post =>
+ M_Elements_Swapped'Result =
+ (M.Length (S1) = M.Length (S2)
+ and Element (S1, X) = Element (S2, Y)
+ and Element (S1, Y) = Element (S2, X)
+ and
+ (for all I in 1 .. M.Length (S1) =>
+ (if I /= X and I /= Y
+ then Element (S1, I) = Element (S2, I))));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
+
+ package P is new Ada.Containers.Functional_Maps
+ (Key_Type => Cursor,
+ Element_Type => Positive_Count_Type,
+ Equivalent_Keys => "=");
+ function "=" (Left, Right : P.Map) return Boolean renames P."=";
+ function "<=" (Left, Right : P.Map) return Boolean renames P."<=";
+
+ function 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
+ ((for all I of Small => P.Mem (Big, I))
+
+ -- 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.Mem (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+
+ function P_Positions_Swapped
+ (M1, M2 : P.Map;
+ C1, C2 : Cursor) return Boolean
+ -- M1 and M2 contain the same cursors, but the positions of C1 and C2
+ -- are reversed.
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ P_Positions_Swapped'Result =
+ ((for all C of M1 => P.Mem (M2, C))
+ and (for all C of M2 => P.Mem (M1, C))
+ and
+ (for all C of M1 =>
+ (if C /= C1 and C /= C2
+ then P.Get (M1, C) = P.Get (M2, C)))
+ and P.Mem (M1, C1) and P.Mem (M1, C2)
+ and P.Get (M1, C1) = P.Get (M2, C2)
+ and P.Get (M1, C2) = P.Get (M2, C1));
+
+ 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
+ ((for all I of Small => P.Mem (Big, I))
+
+ -- The cursors of Small are all bellow Cut
+ and (for all I of Small => P.Get (Small, I) < Cut)
+
+ -- The cursors have the same position in Big and Small
+ and (for all I of Small => P.Get (Big, I) = P.Get (Small, I))
+
+ -- New cursors of Big (if any) are between Cut and Cut - 1 + Count
+ and
+ (for all I of Big =>
+ P.Mem (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+
+ function Mapping_Preserved
+ (S1, S2 : M.Sequence;
+ M1, M2 : P.Map) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved'Result then
+
+ -- M1 contains all cursors of M2
+ (for all I of M2 => P.Mem (M1, I))
+
+ -- M2 contains all cursors of M1
+ and (for all I of M1 => P.Mem (M2, I))
+
+ -- Mappings from cursors to elements induced by S1, M1 and S2, M2
+ -- are the same.
+ and (for all I of M1 =>
+ M.Get (S1, P.Get (M1, I)) = M.Get (S2, P.Get (M2, I))));
+
+ function Model (Container : List) return M.Sequence with
+ -- The highlevel 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.Mem (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 lowlevel, cursor aware view of a container, to a highlevel
+ -- 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;
+ Global => null,
+ Post => "="'Result = (Model (Left) = Model (Right));
- function Length (Container : List) return Count_Type with
- Global => null;
-
function Is_Empty (Container : List) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out List) with
- Global => null;
+ Global => null,
+ Post => Length (Container) = 0;
procedure Assign (Target : in out List; Source : List) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ 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;
+ 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);
+ 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;
@@ -116,229 +382,1007 @@
New_Item : Element_Type)
with
Global => null,
- Pre => Has_Element (Container, Position);
+ 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 replaced by
+ -- New_Item.
+ and M.Is_Set (Model (Container)'Old,
+ P.Get (Positions (Container), Position),
+ New_Item,
+ Model (Container));
+
procedure Move (Target : in out List; Source : in out List) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ 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.Is_Add
+ (Positions (Container)'Old, Last (Container), Length (Container),
+ Result => Positions (Container))
+
+ -- Model contains a new element New_Item at the end
+ and M.Is_Add (Model (Container)'Old, New_Item, Model (Container)),
+ others =>
+
+ -- The elements of Container located before Before are preserved.
+ M_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
+
+ -- Other elements are shifted by 1.
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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 := 1)
+ Count : Count_Type)
with
Global => null,
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ 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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old)
+
+ -- Container contains Count times New_Item at the end
+ and M_Elements_Cst
+ (S => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ E => 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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
+
+ -- Other elements are shifted by Count.
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Cst
+ (S => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst => P.Get (Positions (Container)'Old, Before) - 1 + Count,
+ E => 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;
- Count : Count_Type := 1)
+ Position : out Cursor)
with
Global => null,
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ 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.Mem (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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by 1.
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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 := 1)
+ 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.Mem (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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by Count.
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Cst
+ (S => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => P.Get (Positions (Container), Position) - 1 + Count,
+ E => 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 <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Pre => Length (Container) < Container.Capacity,
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+ -- Elements are shifted by 1
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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 := 1)
+ Count : Count_Type)
with
Global => null,
- Pre => Length (Container) + Count <= Container.Capacity;
+ Pre => Length (Container) <= Container.Capacity - Count,
+ Post =>
+ Length (Container) = Length (Container)'Old + Count
+ -- Elements are shifted by Count.
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container starts with Count times New_Item
+ and M_Elements_Cst
+ (S => Model (Container),
+ Fst => 1,
+ Lst => Count,
+ E => 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.Is_Add
+ (Positions (Container)'Old, Last (Container), Length (Container),
+ Result => Positions (Container))
+
+ -- Model contains a new element New_Item at the end
+ and M.Is_Add (Model (Container)'Old, New_Item, Model (Container));
+
+ procedure Append
+ (Container : in out List;
New_Item : Element_Type;
- Count : Count_Type := 1)
+ Count : Count_Type)
with
Global => null,
- Pre => Length (Container) + Count <= Container.Capacity;
+ 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 M_Elements_Cst
+ (S => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ E => New_Item)
+
+ -- Count cursors have been inserted at the end of Container
+ and P_Positions_Truncated
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Length (Container)'Old + 1,
+ Count => Count);
+
procedure Delete
(Container : in out List;
+ Position : in out Cursor)
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Position is set to No_Element
+ and Position = No_Element
+
+ -- The elements of Container located before Position are preserved.
+ and M_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
+ Lst => Length (Container)'Old,
+ Offset => -1)
+
+ -- Position has been removed from Container
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old));
+
+ procedure Delete
+ (Container : in out List;
Position : in out Cursor;
- Count : Count_Type := 1)
+ 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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst =>
+ P.Get (Positions (Container)'Old, Position'Old) + Count,
+ Lst => Length (Container)'Old,
+ Offset => -Count)
+
+ -- Count cursors have been removed from Container at Position
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old),
+ Count => Count));
+
+ procedure Delete_First (Container : in out List)
+ with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => not Is_Empty (Container),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+ -- The elements of Container are shifted by 1
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 2,
+ Lst => Length (Container)'Old,
+ 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 := 1)
+ Count : Count_Type)
with
- Global => null;
+ 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_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => Count + 1,
+ Lst => Length (Container)'Old,
+ 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 P.Is_Add (Positions (Container), Last (Container)'Old,
+ Length (Container)'Old, Positions (Container)'Old);
+
procedure Delete_Last
(Container : in out List;
- Count : Count_Type := 1)
+ Count : Count_Type)
with
- Global => null;
+ 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;
+ Global => null,
+ Post => M_Elements_Reversed (Model (Container'Old), Model (Container));
procedure Swap
(Container : in out List;
I, J : Cursor)
with
Global => null,
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ 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, J : Cursor)
with
Global => null,
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ 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) + Length (Target) <= Target.Capacity
- and then (Has_Element (Target, Before)
- or else Before = No_Element);
+ 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_Elements_Equal
+ (S1 => Model (Target)'Old,
+ S2 => Model (Target),
+ Fst => 1,
+ Lst => Length (Target)'Old)
+
+ -- The elements of Source are appended to target, the order is not
+ -- specified.
+ and M_Elements_Shuffle
+ (S1 => Model (Source)'Old,
+ S2 => Model (Target),
+ Fst => 1,
+ Lst => Length (Source)'Old,
+ Offset => Length (Target)'Old)
+
+ -- Cursors have been inserted at the end of Target
+ and P_Positions_Truncated
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => Length (Target)'Old + 1,
+ Count => Length (Source)'Old),
+ others =>
+
+ -- The elements of Target located before Before are preserved
+ M_Elements_Equal
+ (S1 => Model (Target)'Old,
+ S2 => 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_Shuffle
+ (S1 => Model (Source)'Old,
+ S2 => Model (Target),
+ Fst => 1,
+ Lst => Length (Source)'Old,
+ Offset => P.Get (Positions (Target)'Old, Before) - 1)
+
+ -- Other elements are shifted by the length of Source
+ and M_Elements_Shifted
+ (S1 => Model (Target)'Old,
+ S2 => 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 => Length (Source) + Length (Target) <= Target.Capacity
- and then (Has_Element (Target, Before)
- or else Before = No_Element)
- and then Has_Element (Source, Position);
+ 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_Elements_Equal
+ (S1 => Model (Source)'Old,
+ S2 => Model (Source),
+ Fst => 1,
+ Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+ and M_Elements_Shifted
+ (S1 => Model (Source)'Old,
+ S2 => 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.Mem (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_Elements_Equal
+ (S1 => Model (Target)'Old,
+ S2 => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target), Position) - 1)
+
+ -- Other elements are shifted by 1.
+ and M_Elements_Shifted
+ (S1 => Model (Target)'Old,
+ S2 => 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 => 2 * Length (Container) <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element)
- and then Has_Element (Container, Position);
+ 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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position) - 1)
+
+ -- The elements located after Position are shifted by 1
+ and M_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ M1 => Positions (Container)'Old,
+ M2 => Positions (Container)),
+
+ others =>
+
+ -- The elements located before Position and Before are preserved
+ M_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Equal
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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_Elements_Shifted
+ (S1 => Model (Container)'Old,
+ S2 => 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
+ (S1 => Model (Container)'Old,
+ S2 => Model (Container),
+ M1 => Positions (Container)'Old,
+ M2 => Positions (Container)));
+
function First (Container : List) return Cursor with
- Global => null;
+ 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);
+ Pre => not Is_Empty (Container),
+ Post => First_Element'Result = M.Get (Model (Container), 1);
function Last (Container : List) return Cursor with
- Global => null;
+ 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);
+ 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;
+ 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;
+ 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;
+ 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;
+ 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;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ -- If Item is not is not contained in Container after Position, Find
+ -- returns No_Element.
+ (not M_Elements_Contains
+ (S => Model (Container),
+ Fst => (if Position = No_Element then 1
+ else P.Get (Positions (Container), Position)),
+ Lst => Length (Container),
+ E => Item)
+ =>
+ Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cusror in Container
+ others =>
+ P.Mem (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 occurence of Item in this slice
+ and not M_Elements_Contains
+ (S => Model (Container),
+ Fst => (if Position = No_Element then 1
+ else P.Get (Positions (Container), Position)),
+ Lst => P.Get (Positions (Container), Find'Result) - 1,
+ E => 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;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ -- If Item is not is not contained in Container before Position, Find
+ -- returns No_Element.
+ (not M_Elements_Contains
+ (S => Model (Container),
+ Fst => 1,
+ Lst => (if Position = No_Element then Length (Container)
+ else P.Get (Positions (Container), Position)),
+ E => Item)
+ =>
+ Reverse_Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cusror in Container
+ others =>
+ P.Mem (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 occurence of Item in this slice
+ and not M_Elements_Contains
+ (S => 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)),
+ E => Item));
+
function Contains
(Container : List;
Item : Element_Type) return Boolean
with
- Global => null;
+ Global => null,
+ Post => Contains'Result =
+ M_Elements_Contains
+ (S => Model (Container),
+ Fst => 1,
+ Lst => Length (Container),
+ E => Item);
function Has_Element (Container : List; Position : Cursor) return Boolean
with
- Global => null;
+ Global => null,
+ Post => Has_Element'Result = P.Mem (Positions (Container), Position);
+ pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode is
+ function M_Elements_Sorted (S : M.Sequence) return Boolean with
+ Ghost,
+ Global => null,
+ Post => M_Elements_Sorted'Result =
+ (for all I in 1 .. M.Length (S) =>
+ (for all J in I + 1 .. M.Length (S) =>
+ Element (S, I) = Element (S, J)
+ or Element (S, I) < Element (S, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : List) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
procedure Sort (Container : in out List) with
- Global => null;
+ Global => null,
+ Post => Length (Container) = Length (Container)'Old
+ and M_Elements_Sorted (Model (Container));
procedure Merge (Target, Source : in out List) with
- Global => null;
-
+ -- 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)));
end Generic_Sorting;
- function Strict_Equal (Left, Right : List) return Boolean with
- Ghost,
- Global => null;
- -- Strict_Equal returns True if the containers are physically equal, i.e.
- -- they are structurally equal (function "=" returns True) and that they
- -- have the same set of cursors.
-
- function First_To_Previous (Container : List; Current : Cursor) return List
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
-
- function Current_To_Last (Container : List; Current : Cursor) return List
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
- -- First_To_Previous returns a container containing all elements preceding
- -- Current (excluded) in Container. Current_To_Last returns a container
- -- containing all elements following Current (included) in Container.
- -- These two new functions can be used to express invariant properties in
- -- loops which iterate over containers. First_To_Previous returns the part
- -- of the container already scanned and Current_To_Last the part not
- -- scanned yet.
-
private
pragma SPARK_Mode (Off);
@@ -361,12 +1405,6 @@
Nodes : Node_Array (1 .. Capacity) := (others => <>);
end record;
- type Cursor is record
- Node : Count_Type := 0;
- end record;
-
Empty_List : constant List := (0, others => <>);
- No_Element : constant Cursor := (Node => 0);
-
end Ada.Containers.Formal_Doubly_Linked_Lists;
More information about the Gcc-patches
mailing list