| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT LIBRARY COMPONENTS -- |
| -- -- |
| -- ADA.CONTAINERS.FUNCTIONAL_VECTORS -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 2016-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/>. -- |
| ------------------------------------------------------------------------------ |
| |
| pragma Ada_2012; |
| private with Ada.Containers.Functional_Base; |
| |
| generic |
| type Index_Type is (<>); |
| -- To avoid Constraint_Error being raised at run time, Index_Type'Base |
| -- should have at least one more element at the low end than Index_Type. |
| |
| type Element_Type (<>) is private; |
| with function "=" (Left, Right : Element_Type) return Boolean is <>; |
| |
| package Ada.Containers.Functional_Vectors with SPARK_Mode is |
| |
| subtype Extended_Index is Index_Type'Base range |
| Index_Type'Pred (Index_Type'First) .. Index_Type'Last; |
| -- Index_Type with one more element at the low end of the range. |
| -- This type is never used but it forces GNATprove to check that there is |
| -- room for one more element at the low end of Index_Type. |
| |
| type Sequence is private |
| with Default_Initial_Condition => Length (Sequence) = 0, |
| Iterable => (First => Iter_First, |
| Has_Element => Iter_Has_Element, |
| Next => Iter_Next, |
| Element => Get); |
| -- Sequences are empty when default initialized. |
| -- Quantification over sequences can be done using the regular |
| -- quantification over its range or directly on its elements with "for of". |
| |
| ----------------------- |
| -- Basic operations -- |
| ----------------------- |
| |
| -- Sequences are axiomatized using Length and Get, providing respectively |
| -- the length of a sequence and an accessor to its Nth element: |
| |
| function Length (Container : Sequence) return Count_Type with |
| -- Length of a sequence |
| |
| Global => null, |
| Post => |
| (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= |
| Index_Type'Pos (Index_Type'Last); |
| |
| function Get |
| (Container : Sequence; |
| Position : Extended_Index) return Element_Type |
| -- Access the Element at position Position in Container |
| |
| with |
| Global => null, |
| Pre => Position in Index_Type'First .. Last (Container); |
| |
| function Last (Container : Sequence) return Extended_Index with |
| -- Last index of a sequence |
| |
| Global => null, |
| Post => |
| Last'Result = |
| Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + |
| Length (Container)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Last); |
| |
| function First return Extended_Index is (Index_Type'First) with |
| Global => null; |
| -- First index of a sequence |
| |
| ------------------------ |
| -- Property Functions -- |
| ------------------------ |
| |
| function "=" (Left : Sequence; Right : Sequence) return Boolean with |
| -- Extensional equality over sequences |
| |
| Global => null, |
| Post => |
| "="'Result = |
| (Length (Left) = Length (Right) |
| and then (for all N in Index_Type'First .. Last (Left) => |
| Get (Left, N) = Get (Right, N))); |
| pragma Annotate (GNATprove, Inline_For_Proof, "="); |
| |
| function "<" (Left : Sequence; Right : Sequence) return Boolean with |
| -- Left is a strict subsequence of Right |
| |
| Global => null, |
| Post => |
| "<"'Result = |
| (Length (Left) < Length (Right) |
| and then (for all N in Index_Type'First .. Last (Left) => |
| Get (Left, N) = Get (Right, N))); |
| pragma Annotate (GNATprove, Inline_For_Proof, "<"); |
| |
| function "<=" (Left : Sequence; Right : Sequence) return Boolean with |
| -- Left is a subsequence of Right |
| |
| Global => null, |
| Post => |
| "<="'Result = |
| (Length (Left) <= Length (Right) |
| and then (for all N in Index_Type'First .. Last (Left) => |
| Get (Left, N) = Get (Right, N))); |
| pragma Annotate (GNATprove, Inline_For_Proof, "<="); |
| |
| function Contains |
| (Container : Sequence; |
| Fst : Index_Type; |
| Lst : Extended_Index; |
| Item : Element_Type) return Boolean |
| -- Returns True if Item occurs in the range from Fst to Lst of Container |
| |
| with |
| Global => null, |
| Pre => Lst <= Last (Container), |
| Post => |
| Contains'Result = |
| (for some I in Fst .. Lst => Get (Container, I) = Item); |
| pragma Annotate (GNATprove, Inline_For_Proof, Contains); |
| |
| function Constant_Range |
| (Container : Sequence; |
| Fst : Index_Type; |
| Lst : Extended_Index; |
| Item : Element_Type) return Boolean |
| -- Returns True if every element of the range from Fst to Lst of Container |
| -- is equal to Item. |
| |
| with |
| Global => null, |
| Pre => Lst <= Last (Container), |
| Post => |
| Constant_Range'Result = |
| (for all I in Fst .. Lst => Get (Container, I) = Item); |
| pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range); |
| |
| function Equal_Except |
| (Left : Sequence; |
| Right : Sequence; |
| Position : Index_Type) return Boolean |
| -- Returns True is Left and Right are the same except at position Position |
| |
| with |
| Global => null, |
| Pre => Position <= Last (Left), |
| Post => |
| Equal_Except'Result = |
| (Length (Left) = Length (Right) |
| and then (for all I in Index_Type'First .. Last (Left) => |
| (if I /= Position then Get (Left, I) = Get (Right, I)))); |
| pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); |
| |
| function Equal_Except |
| (Left : Sequence; |
| Right : Sequence; |
| X : Index_Type; |
| Y : Index_Type) return Boolean |
| -- Returns True is Left and Right are the same except at positions X and Y |
| |
| with |
| Global => null, |
| Pre => X <= Last (Left) and Y <= Last (Left), |
| Post => |
| Equal_Except'Result = |
| (Length (Left) = Length (Right) |
| and then (for all I in Index_Type'First .. Last (Left) => |
| (if I /= X and I /= Y then |
| Get (Left, I) = Get (Right, I)))); |
| pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); |
| |
| function Range_Equal |
| (Left : Sequence; |
| Right : Sequence; |
| Fst : Index_Type; |
| Lst : Extended_Index) return Boolean |
| -- Returns True if the ranges from Fst to Lst contain the same elements in |
| -- Left and Right. |
| |
| with |
| Global => null, |
| Pre => Lst <= Last (Left) and Lst <= Last (Right), |
| Post => |
| Range_Equal'Result = |
| (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal); |
| |
| function Range_Shifted |
| (Left : Sequence; |
| Right : Sequence; |
| Fst : Index_Type; |
| Lst : Extended_Index; |
| Offset : Count_Type'Base) return Boolean |
| -- Returns True if the range from Fst to Lst in Left contains the same |
| -- elements as the range from Fst + Offset to Lst + Offset in Right. |
| |
| with |
| Global => null, |
| Pre => |
| Lst <= Last (Left) |
| and then |
| (if Offset < 0 then |
| Index_Type'Pos (Index_Type'Base'First) - Offset <= |
| Index_Type'Pos (Index_Type'First)) |
| and then |
| (if Fst <= Lst then |
| Offset in |
| Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. |
| (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - |
| Index_Type'Pos (Lst)), |
| Post => |
| Range_Shifted'Result = |
| ((for all I in Fst .. Lst => |
| Get (Left, I) = |
| Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) |
| and |
| (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) .. |
| Index_Type'Val (Index_Type'Pos (Lst) + Offset) |
| => |
| Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) = |
| Get (Right, I))); |
| pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted); |
| |
| ---------------------------- |
| -- Construction Functions -- |
| ---------------------------- |
| |
| -- For better efficiency of both proofs and execution, avoid using |
| -- construction functions in annotations and rather use property functions. |
| |
| function Set |
| (Container : Sequence; |
| Position : Index_Type; |
| New_Item : Element_Type) return Sequence |
| -- Returns a new sequence which contains the same elements as Container |
| -- except for the one at position Position which is replaced by New_Item. |
| |
| with |
| Global => null, |
| Pre => Position in Index_Type'First .. Last (Container), |
| Post => |
| Get (Set'Result, Position) = New_Item |
| and then Equal_Except (Container, Set'Result, Position); |
| |
| function Add (Container : Sequence; New_Item : Element_Type) return Sequence |
| -- Returns a new sequence which contains the same elements as Container |
| -- plus New_Item at the end. |
| |
| with |
| Global => null, |
| Pre => |
| Length (Container) < Count_Type'Last |
| and then Last (Container) < Index_Type'Last, |
| Post => |
| Length (Add'Result) = Length (Container) + 1 |
| and then Get (Add'Result, Last (Add'Result)) = New_Item |
| and then Container <= Add'Result; |
| |
| function Add |
| (Container : Sequence; |
| Position : Index_Type; |
| New_Item : Element_Type) return Sequence |
| with |
| -- Returns a new sequence which contains the same elements as Container |
| -- except that New_Item has been inserted at position Position. |
| |
| Global => null, |
| Pre => |
| Length (Container) < Count_Type'Last |
| and then Last (Container) < Index_Type'Last |
| and then Position <= Extended_Index'Succ (Last (Container)), |
| Post => |
| Length (Add'Result) = Length (Container) + 1 |
| and then Get (Add'Result, Position) = New_Item |
| and then Range_Equal |
| (Left => Container, |
| Right => Add'Result, |
| Fst => Index_Type'First, |
| Lst => Index_Type'Pred (Position)) |
| and then Range_Shifted |
| (Left => Container, |
| Right => Add'Result, |
| Fst => Position, |
| Lst => Last (Container), |
| Offset => 1); |
| |
| function Remove |
| (Container : Sequence; |
| Position : Index_Type) return Sequence |
| -- Returns a new sequence which contains the same elements as Container |
| -- except that the element at position Position has been removed. |
| |
| with |
| Global => null, |
| Pre => Position in Index_Type'First .. Last (Container), |
| Post => |
| Length (Remove'Result) = Length (Container) - 1 |
| and then Range_Equal |
| (Left => Container, |
| Right => Remove'Result, |
| Fst => Index_Type'First, |
| Lst => Index_Type'Pred (Position)) |
| and then Range_Shifted |
| (Left => Remove'Result, |
| Right => Container, |
| Fst => Position, |
| Lst => Last (Remove'Result), |
| Offset => 1); |
| |
| function Copy_Element (Item : Element_Type) return Element_Type is (Item); |
| -- Elements of containers are copied by numerous primitives in this |
| -- package. This function causes GNATprove to verify that such a copy is |
| -- valid (in particular, it does not break the ownership policy of SPARK, |
| -- i.e. it does not contain pointers that could be used to alias mutable |
| -- data). |
| |
| --------------------------- |
| -- Iteration Primitives -- |
| --------------------------- |
| |
| function Iter_First (Container : Sequence) return Extended_Index with |
| Global => null; |
| |
| function Iter_Has_Element |
| (Container : Sequence; |
| Position : Extended_Index) return Boolean |
| with |
| Global => null, |
| Post => |
| Iter_Has_Element'Result = |
| (Position in Index_Type'First .. Last (Container)); |
| pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); |
| |
| function Iter_Next |
| (Container : Sequence; |
| Position : Extended_Index) return Extended_Index |
| with |
| Global => null, |
| Pre => Iter_Has_Element (Container, Position); |
| |
| private |
| |
| pragma SPARK_Mode (Off); |
| |
| package Containers is new Ada.Containers.Functional_Base |
| (Index_Type => Index_Type, |
| Element_Type => Element_Type); |
| |
| type Sequence is record |
| Content : Containers.Container; |
| end record; |
| |
| function Iter_First (Container : Sequence) return Extended_Index is |
| (Index_Type'First); |
| |
| function Iter_Next |
| (Container : Sequence; |
| Position : Extended_Index) return Extended_Index |
| is |
| (if Position = Extended_Index'Last then |
| Extended_Index'First |
| else |
| Extended_Index'Succ (Position)); |
| |
| function Iter_Has_Element |
| (Container : Sequence; |
| Position : Extended_Index) return Boolean |
| is |
| (Position in Index_Type'First .. |
| (Index_Type'Val |
| ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); |
| |
| end Ada.Containers.Functional_Vectors; |
