blob: ee5273039d391b693206e81392a5b348155ec10b [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_VECTORS --
-- --
-- S p e c --
-- --
-- Copyright (C) 2016-2021, 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;