diff mbox

[Ada] Provide library for functional containers

Message ID 20170427090707.GA79844@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 27, 2017, 9:07 a.m. UTC
This patch introduces new children of Ada.Containers. They provide
functional, mathematical like containers, which can be used as high
level models when specifying data structures.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cofuba.ads, a-cofuba.adb (Ada.Containers.Functional_Base): New
	private child of Ada.Containers used to implement all functional
	containers.
	* a-cofuma.ads, a-cofuma.adb (Ada.Containers.Functional_Maps): New
	child of Ada.Containers. It provides functional indefinite unbounded
	maps which can be used as high level models for specification
	of data structures.
	* a-cofuse.ads, a-cofuse.adb (Ada.Containers.Functional_Sets): New
	child of Ada.Containers. It provides functional indefinite unbounded
	sets which can be used as high level models for specification
	of data structures.
	* a-cofuve.ads, a-cofuve.adb (Ada.Containers.Functional_Vectors): New
	child of Ada.Containers.  It provides functional indefinite unbounded
	vectors which can be used as high level models for specification
	of data structures.
	* Makefile.rtl: Add new packages.
	* impunit.adb: Add new packages.
diff mbox

Patch

Index: impunit.adb
===================================================================
--- impunit.adb	(revision 247293)
+++ impunit.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---           Copyright (C) 2000-2016, Free Software Foundation, Inc.        --
+--           Copyright (C) 2000-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- --
@@ -590,6 +590,9 @@ 
     ("a-cfinve", F),  -- Ada.Containers.Formal_Indefinite_Vectors
     ("a-coboho", F),  -- Ada.Containers.Bounded_Holders
     ("a-cofove", F),  -- Ada.Containers.Formal_Vectors
+    ("a-cofuma", F),  -- Ada.Containers.Functional_Maps
+    ("a-cofuse", F),  -- Ada.Containers.Functional_Sets
+    ("a-cofuve", F),  -- Ada.Containers.Functional_Vectors
     ("a-cfdlli", F),  -- Ada.Containers.Formal_Doubly_Linked_Lists
     ("a-cforse", F),  -- Ada.Containers.Formal_Ordered_Sets
     ("a-cforma", F),  -- Ada.Containers.Formal_Ordered_Maps
Index: a-cofuse.adb
===================================================================
--- a-cofuse.adb	(revision 0)
+++ a-cofuse.adb	(revision 0)
@@ -0,0 +1,128 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_SETS                      --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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;
+
+package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
+   use Containers;
+
+   pragma Assertion_Policy
+      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
+
+   ---------
+   -- "=" --
+   ---------
+
+   function "=" (S1, S2 : Set) return Boolean is
+     (S1.Content <= S2.Content and S2.Content <= S1.Content);
+
+   ----------
+   -- "<=" --
+   ----------
+
+   function "<=" (S1, S2 : Set) return Boolean is (S1.Content <= S2.Content);
+
+   ---------
+   -- Add --
+   ---------
+
+   function Add (S : Set; E : Element_Type) return Set is
+     (Content => Add (S.Content, E));
+
+   ------------
+   -- Length --
+   ------------
+
+   function Length (S : Set) return Count_Type is (Length (S.Content));
+
+   ---------
+   -- Mem --
+   ---------
+
+   function Mem (S : Set; E : Element_Type) return Boolean is
+      (Find (S.Content, E) > 0);
+
+   ------------------
+   -- Num_Overlaps --
+   ------------------
+
+   function Num_Overlaps (S1, S2 : Set) return Count_Type is
+      (Num_Overlaps (S1.Content, S2.Content));
+
+   ------------------
+   -- Intersection --
+   ------------------
+
+   function Intersection (S1, S2 : Set) return Set is
+     (Content => Intersection (S1.Content, S2.Content));
+
+   ------------
+   -- Is_Add --
+   ------------
+
+   function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
+   is
+     (Mem (Result, E)
+      and (for all F of Result => Mem (S, F) or F = E)
+      and (for all E of S => Mem (Result, E)));
+
+   --------------
+   -- Is_Empty --
+   --------------
+
+   function Is_Empty (S : Set) return Boolean is (Length (S.Content) = 0);
+
+   ---------------------
+   -- Is_Intersection --
+   ---------------------
+
+   function Is_Intersection (S1, S2, Result : Set) return Boolean is
+     ((for all E of Result =>
+            Mem (S1, E) and Mem (S2, E))
+      and (for all E of S1 =>
+               (if Mem (S2, E) then Mem (Result, E))));
+
+   --------------
+   -- Is_Union --
+   --------------
+
+   function Is_Union (S1, S2, Result : Set) return Boolean is
+     ((for all E of Result => Mem (S1, E) or Mem (S2, E))
+      and (for all E of S1 => Mem (Result, E))
+      and (for all E of S2 => Mem (Result, E)));
+
+   -----------
+   -- Union --
+   -----------
+
+   function Union (S1, S2 : Set) return Set is
+     (Content => Union (S1.Content, S2.Content));
+end Ada.Containers.Functional_Sets;
Index: a-cofuse.ads
===================================================================
--- a-cofuse.ads	(revision 0)
+++ a-cofuse.ads	(revision 0)
@@ -0,0 +1,195 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_SETS                      --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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 Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+package Ada.Containers.Functional_Sets with SPARK_Mode is
+
+   type Set is private with
+     Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0,
+     Iterable                  => (First       => Iter_First,
+                                   Next        => Iter_Next,
+                                   Has_Element => Iter_Has_Element,
+                                   Element     => Iter_Element);
+   --  Sets are empty when default initialized.
+   --  For in quantification over sets should not be used.
+   --  For of quantification over sets iterates over elements.
+
+   --  Sets are axiomatized using Mem which encodes whether an element is
+   --  contained in a set.  The length of a set is also added to protect Add
+   --  against overflows but it is not actually modeled.
+
+   function Mem (S : Set; E : Element_Type) return Boolean with
+     Global => null;
+
+   function Length (S : Set) return Count_Type with
+     Global => null;
+
+   function "<=" (S1, S2 : Set) return Boolean with
+   --  Set inclusion.
+
+     Global => null,
+     Post   => "<="'Result = (for all E of S1 => Mem (S2, E));
+
+   function "=" (S1, S2 : Set) return Boolean with
+   --  Extensional equality over sets.
+
+     Global => null,
+     Post   =>
+       "="'Result = ((for all E of S1 => Mem (S2, E))
+                     and (for all E of S2 => Mem (S1, E)));
+
+   pragma Warnings (Off, "unused variable ""E""");
+   function Is_Empty (S : Set) return Boolean with
+   --  A set is empty if it contains no element.
+
+     Global => null,
+     Post   => Is_Empty'Result = (for all E of S => False);
+   pragma Warnings (On, "unused variable ""E""");
+
+   function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
+   --  Returns True if Result is S augmented with E.
+
+   with
+     Global => null,
+     Post   => Is_Add'Result =
+       (Mem (Result, E) and not Mem (S, E)
+        and (for all F of Result => Mem (S, F) or F = E)
+        and (for all E of S => Mem (Result, E)));
+
+   function Add (S : Set; E : Element_Type) return Set with
+   --  Returns S augmented with E.
+   --  Is_Add (S, E, Result) should be used instead of Result = Add (S, E)
+   --  whenever possible both for execution and for proof.
+
+     Global => null,
+     Pre    => not Mem (S, E) and Length (S) < Count_Type'Last,
+     Post   => Length (Add'Result) = Length (S) + 1
+     and Is_Add (S, E, Add'Result);
+
+   function Is_Intersection (S1, S2, Result : Set) return Boolean with
+   --  Returns True if Result is the intersection of S1 and S2.
+
+     Global => null,
+     Post   => Is_Intersection'Result =
+       ((for all E of Result =>
+               Mem (S1, E) and Mem (S2, E))
+        and (for all E of S1 =>
+               (if Mem (S2, E) then Mem (Result, E))));
+
+   function Num_Overlaps (S1, S2 : Set) return Count_Type with
+   --  Number of elements that are both in S1 and S2.
+
+     Global => null,
+     Post   => Num_Overlaps'Result <= Length (S1)
+     and Num_Overlaps'Result <= Length (S2)
+     and (if Num_Overlaps'Result = 0 then
+            (for all E of S1 => not Mem (S2, E)));
+
+   function Intersection (S1, S2 : Set) return Set with
+   --  Returns the intersection of S1 and S2.
+   --  Intersection (S1, S2, Result) should be used instead of
+   --  Result = Intersection (S1, S2) whenever possible both for execution and
+   --  for proof.
+
+     Global => null,
+     Post   => Length (Intersection'Result) = Num_Overlaps (S1, S2)
+     and Is_Intersection (S1, S2, Intersection'Result);
+
+   function Is_Union (S1, S2, Result : Set) return Boolean with
+   --  Returns True if Result is the union of S1 and S2.
+
+     Global => null,
+     Post   => Is_Union'Result =
+       ((for all E of Result => Mem (S1, E) or Mem (S2, E))
+        and (for all E of S1 => Mem (Result, E))
+        and (for all E of S2 => Mem (Result, E)));
+
+   function Union (S1, S2 : Set) return Set with
+   --  Returns the union of S1 and S2.
+   --  Is_Union (S1, S2, Result) should be used instead of
+   --  Result = Union (S1, S2) whenever possible both for execution and for
+   --  proof.
+
+     Global => null,
+     Pre    => Length (S1) - Num_Overlaps (S1, S2) <=
+     Count_Type'Last - Length (S2),
+     Post   => Length (Union'Result) = Length (S1) - Num_Overlaps (S1, S2)
+     + Length (S2)
+     and Is_Union (S1, S2, Union'Result);
+
+   ---------------------------
+   --  Iteration Primitives --
+   ---------------------------
+
+   type Private_Key is private;
+
+   function Iter_First (S : Set) return Private_Key with
+     Global => null;
+   function Iter_Has_Element (S : Set; K : Private_Key) return Boolean with
+     Global => null;
+   function Iter_Next (S : Set; K : Private_Key) return Private_Key with
+     Global => null,
+     Pre    => Iter_Has_Element (S, K);
+   function Iter_Element (S : Set; K : Private_Key) return Element_Type with
+     Global => null,
+     Pre    => Iter_Has_Element (S, K);
+   pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+private
+   pragma SPARK_Mode (Off);
+
+   subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+   package Containers is new Ada.Containers.Functional_Base
+     (Element_Type        => Element_Type,
+      Index_Type          => Positive_Count_Type);
+
+   type Set is record
+      Content : Containers.Container;
+   end record;
+
+   type Private_Key is new Count_Type;
+
+   function Iter_First (S : Set) return Private_Key is (1);
+
+   function Iter_Has_Element (S : Set; K : Private_Key) return Boolean is
+     (Count_Type (K) in 1 .. Containers.Length (S.Content));
+
+   function Iter_Next (S : Set; K : Private_Key) return Private_Key is
+     (if K = Private_Key'Last then 0 else K + 1);
+
+   function Iter_Element (S : Set; K : Private_Key) return Element_Type is
+     (Containers.Get (S.Content, Count_Type (K)));
+end Ada.Containers.Functional_Sets;
Index: Makefile.rtl
===================================================================
--- Makefile.rtl	(revision 247293)
+++ Makefile.rtl	(working copy)
@@ -137,6 +137,10 @@ 
   a-coboho$(objext) \
   a-cobove$(objext) \
   a-cofove$(objext) \
+  a-cofuba$(objext) \
+  a-cofuma$(objext) \
+  a-cofuse$(objext) \
+  a-cofuve$(objext) \
   a-cogeso$(objext) \
   a-cohama$(objext) \
   a-cohase$(objext) \
Index: a-cofuve.adb
===================================================================
--- a-cofuve.adb	(revision 0)
+++ a-cofuve.adb	(revision 0)
@@ -0,0 +1,133 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                    ADA.CONTAINERS.FUNCTIONAL_VECTORS                     --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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;
+package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
+   use Containers;
+
+   pragma Assertion_Policy
+      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
+
+   ---------
+   -- "=" --
+   ---------
+
+   function "=" (S1, S2 : Sequence) return Boolean is
+     (S1.Content = S2.Content);
+
+   ---------
+   -- "<" --
+   ---------
+
+   function "<" (S1, S2 : Sequence) return Boolean is
+     (Length (S1.Content) < Length (S2.Content)
+      and then (for all I in Index_Type'First .. Last (S1) =>
+                   Get (S1.Content, I) = Get (S2.Content, I)));
+
+   ----------
+   -- "<=" --
+   ----------
+
+   function "<=" (S1, S2 : Sequence) return Boolean is
+     (Length (S1.Content) <= Length (S2.Content)
+      and then (for all I in Index_Type'First .. Last (S1) =>
+                   Get (S1.Content, I) = Get (S2.Content, I)));
+
+   ---------
+   -- Add --
+   ---------
+
+   function Add (S : Sequence; E : Element_Type) return Sequence is
+     (Content => Add (S.Content, E));
+
+   ---------
+   -- Get --
+   ---------
+
+   function Get (S : Sequence; N : Extended_Index) return Element_Type is
+     (Get (S.Content, N));
+
+   ------------
+   -- Is_Add --
+   ------------
+
+   function Is_Add
+     (S : Sequence; E : Element_Type; Result : Sequence) return Boolean is
+     (Length (Result) = Length (S) + 1
+      and then Get (Result, Index_Type'Val
+                    ((Index_Type'Pos (Index_Type'First) - 1) +
+                       Length (Result))) = E
+      and then
+        (for all M in Index_Type'First ..
+             (Index_Type'Val
+                  ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) =>
+              Get (Result, M) = Get (S, M)));
+
+   ------------
+   -- Is_Set --
+   ------------
+
+   function Is_Set
+     (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence)
+      return Boolean is
+     (N in Index_Type'First ..
+             (Index_Type'Val
+                  ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))
+      and then Length (Result) = Length (S)
+      and then Get (Result, N) = E
+      and then
+        (for all M in  Index_Type'First ..
+             (Index_Type'Val
+                  ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) =>
+             (if M /= N then Get (Result, M) = Get (S, M))));
+
+   ----------
+   -- Last --
+   ----------
+
+   function Last (S : Sequence) return Extended_Index is
+     (Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)));
+
+   ------------
+   -- Length --
+   ------------
+
+   function Length (S : Sequence) return Count_Type is
+     (Length (S.Content));
+
+   ---------
+   -- Set --
+   ---------
+
+   function Set (S : Sequence; N : Index_Type; E : Element_Type)
+                 return Sequence is
+     (Content => Set (S.Content, N, E));
+end Ada.Containers.Functional_Vectors;
Index: a-cofuve.ads
===================================================================
--- a-cofuve.ads	(revision 0)
+++ a-cofuve.ads	(revision 0)
@@ -0,0 +1,198 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                    ADA.CONTAINERS.FUNCTIONAL_VECTORS                     --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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 runtime, Index_Type'Base
+   --  should have at least one more element at the left 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 to the left.
+   --  This type is never used but it forces GNATprove to check that there is
+   --  room for one more element at the left 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 directky on its elements using for of.
+
+   --  Sequences are axiomatized using Length and Get providing respectively
+   --  the length of a sequence and an accessor to its Nth element:
+
+   function Length (S : Sequence) return Count_Type with
+     Global => null,
+     Post => (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
+       Index_Type'Pos (Index_Type'Last);
+
+   function Last (S : Sequence) return Extended_Index with
+     Global => null,
+     Post => Last'Result =
+       Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S));
+
+   function First return Extended_Index is (Index_Type'First);
+
+   function Get (S : Sequence; N : Extended_Index) return Element_Type
+   --  Get ranges over Extended_Index so that it can be used for iteration.
+
+   with
+     Global => null,
+     Pre    => N in Index_Type'First .. Last (S);
+
+   function "=" (S1, S2 : Sequence) return Boolean with
+   --  Extensional equality over sequences.
+
+     Global => null,
+     Post   => "="'Result =
+       (Length (S1) = Length (S2)
+        and then (for all N in Index_Type'First .. Last (S1) =>
+            Get (S1, N) = Get (S2, N)));
+
+   function "<" (S1, S2 : Sequence) return Boolean with
+   --  S1 is a strict subsequence of S2
+
+     Global => null,
+     Post   => "<"'Result =
+     (Length (S1) < Length (S2)
+      and then (for all N in Index_Type'First .. Last (S1) =>
+          Get (S1, N) = Get (S2, N)));
+
+   function "<=" (S1, S2 : Sequence) return Boolean with
+   --  S1 is a subsequence of S2
+
+     Global => null,
+     Post   => "<="'Result =
+     (Length (S1) <= Length (S2)
+      and then (for all N in Index_Type'First .. Last (S1) =>
+          Get (S1, N) = Get (S2, N)));
+
+   function Is_Set
+     (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence)
+      return Boolean
+   --  Returns True if Result is S where the Nth element has been replaced by
+   --  E.
+
+   with
+     Global => null,
+       Post   => Is_Set'Result =
+         (N in Index_Type'First .. Last (S)
+          and then Length (Result) = Length (S)
+          and then Get (Result, N) = E
+          and then (for all M in Index_Type'First .. Last (S) =>
+              (if M /= N then Get (Result, M) = Get (S, M))));
+
+   function Set
+     (S : Sequence; N : Index_Type; E : Element_Type) return Sequence
+   --  Returns S where the Nth element has been replaced by E.
+   --  Is_Set (S, N, E, Result) should be instead of than
+   --  Result = Set (S, N, E) whenever possible both for execution and for
+   --  proof.
+
+   with
+     Global => null,
+     Pre    => N in Index_Type'First .. Last (S),
+     Post   => Is_Set (S, N, E, Set'Result);
+
+   function Is_Add
+     (S : Sequence; E : Element_Type; Result : Sequence) return Boolean
+   --  Returns True if Result is S appended with E.
+
+   with
+     Global => null,
+     Post   => Is_Add'Result =
+         (Length (Result) = Length (S) + 1
+          and then Get (Result, Last (Result)) = E
+          and then (for all M in Index_Type'First .. Last (S) =>
+              Get (Result, M) = Get (S, M)));
+
+   function Add (S : Sequence; E : Element_Type) return Sequence with
+   --  Returns S appended with E.
+   --  Is_Add (S, E, Result) should be used instead of Result = Add (S, E)
+   --  whenever possible both for execution and for proof.
+
+     Global => null,
+     Pre    => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last,
+     Post   => Is_Add (S, E, Add'Result);
+
+   ---------------------------
+   --  Iteration Primitives --
+   ---------------------------
+
+   function Iter_First (S : Sequence) return Extended_Index with
+     Global => null;
+   function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean
+   with
+     Global => null,
+     Post   => Iter_Has_Element'Result = (I in Index_Type'First .. Last (S));
+   pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
+
+   function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index
+   with
+     Global => null,
+     Pre    => Iter_Has_Element (S, I);
+
+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 (S :
+                        Sequence) return Extended_Index
+   is (Index_Type'First);
+   function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index
+   is
+     (if I = Extended_Index'Last then Extended_Index'First
+      else Extended_Index'Succ (I));
+
+   function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean
+   is
+     (I in Index_Type'First ..
+        (Index_Type'Val
+             ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))));
+end Ada.Containers.Functional_Vectors;
Index: a-cofuma.adb
===================================================================
--- a-cofuma.adb	(revision 0)
+++ a-cofuma.adb	(revision 0)
@@ -0,0 +1,161 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_MAPS                      --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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;
+package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
+   use Key_Containers;
+   use Element_Containers;
+
+   pragma Assertion_Policy
+      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
+
+   ---------
+   -- "=" --
+   ---------
+
+   function "=" (M1, M2 : Map) return Boolean is
+     (M1.Keys <= M2.Keys and M2 <= M1);
+
+   ----------
+   -- "<=" --
+   ----------
+
+   function "<=" (M1, M2 : Map) return Boolean is
+      I2 : Count_Type;
+   begin
+      for I1 in 1 .. Length (M1.Keys) loop
+         I2 := Find (M2.Keys, Get (M1.Keys, I1));
+         if I2 = 0
+           or else Get (M2.Elements, I2) /= Get (M1.Elements, I1)
+         then
+            return False;
+         end if;
+      end loop;
+      return True;
+   end "<=";
+
+   ---------
+   -- Add --
+   ---------
+
+   function Add (M : Map; K : Key_Type; E : Element_Type) return Map is
+   begin
+      return
+        (Keys     => Add (M.Keys, K),
+         Elements => Add (M.Elements, E));
+   end Add;
+
+   ---------
+   -- Get --
+   ---------
+
+   function Get (M : Map; K : Key_Type) return Element_Type is
+   begin
+      return Get (M.Elements, Find (M.Keys, K));
+   end Get;
+
+   ------------
+   -- Is_Add --
+   ------------
+
+   function Is_Add
+     (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
+   is
+   begin
+      if Mem (M, K) or not Mem (Result, K) or Get (Result, K) /= E then
+         return False;
+      end if;
+
+      for K of M loop
+         if not Mem (Result, K) or else Get (Result, K) /= Get (M, K) then
+            return False;
+         end if;
+      end loop;
+
+      for KK of Result loop
+         if KK /= K and not Mem (M, KK) then
+            return False;
+         end if;
+      end loop;
+
+      return True;
+   end Is_Add;
+
+   --------------
+   -- Is_Empty --
+   --------------
+
+   function Is_Empty (M : Map) return Boolean is
+   begin
+      return Length (M.Keys) = 0;
+   end Is_Empty;
+
+   ------------
+   -- Is_Set --
+   ------------
+
+   function Is_Set
+     (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
+   is
+     (Mem (M, K)
+      and then Mem (Result, K)
+      and then Get (Result, K) = E
+      and then (for all KK of M => Mem (Result, KK)
+                and then
+                  (if K /= KK
+                   then Get (Result, KK) = Get (M, KK)))
+      and then (for all K of Result => Mem (M, K)));
+
+   ------------
+   -- Length --
+   ------------
+
+   function Length (M : Map) return Count_Type is
+   begin
+      return Length (M.Elements);
+   end Length;
+
+   ---------
+   -- Mem --
+   ---------
+
+   function Mem (M : Map; K : Key_Type) return Boolean is
+   begin
+      return Find (M.Keys, K) > 0;
+   end Mem;
+
+   ---------
+   -- Set --
+   ---------
+
+   function Set (M : Map; K : Key_Type; E : Element_Type) return Map is
+     (Keys => M.Keys, Elements => Set (M.Elements, Find (M.Keys, K), E));
+end Ada.Containers.Functional_Maps;
Index: a-cofuma.ads
===================================================================
--- a-cofuma.ads	(revision 0)
+++ a-cofuma.ads	(revision 0)
@@ -0,0 +1,193 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_MAPS                      --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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 Key_Type (<>) is private;
+   type Element_Type (<>)  is private;
+   with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+package Ada.Containers.Functional_Maps with SPARK_Mode is
+
+   type Map is private with
+     Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
+     Iterable                  => (First       => Iter_First,
+                                   Next        => Iter_Next,
+                                   Has_Element => Iter_Has_Element,
+                                   Element     => Iter_Element);
+   --  Maps are empty when default initialized.
+   --  For in quantification over maps should not be used.
+   --  For of quantification over maps iterates over keys.
+
+   --  Maps are axiomatized using Mem and Get encoding respectively the
+   --  presence of a key in a map and an accessor to elements associated to its
+   --  keys. The length of a map is also added to protect Add against overflows
+   --  but it is not actually modeled.
+
+   function Mem (M : Map; K : Key_Type) return Boolean with
+     Global => null;
+   function Get (M : Map; K : Key_Type) return Element_Type with
+     Global => null,
+     Pre    => Mem (M, K);
+
+   function Length (M : Map) return Count_Type with
+     Global => null;
+
+   function "<=" (M1, M2 : Map) return Boolean with
+   --  Map inclusion.
+
+     Global => null,
+     Post   => "<="'Result =
+       (for all K of M1 => Mem (M2, K)
+        and then Get (M2, K) = Get (M1, K));
+
+   function "=" (M1, M2 : Map) return Boolean with
+   --  Extensional equality over maps.
+
+     Global => null,
+     Post   => "="'Result =
+       ((for all K of M1 => Mem (M2, K)
+        and then Get (M2, K) = Get (M1, K))
+        and (for all K of M2 => Mem (M1, K)));
+
+   pragma Warnings (Off, "unused variable ""K""");
+   function Is_Empty (M : Map) return Boolean with
+   --  A map is empty if it contains no key.
+
+     Global => null,
+     Post   => Is_Empty'Result = (for all K of M => False);
+   pragma Warnings (On, "unused variable ""K""");
+
+   function Is_Add
+     (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
+   --  Returns True if Result is M augmented with the mapping K -> E.
+
+   with
+     Global => null,
+     Post   => Is_Add'Result =
+         (not Mem (M, K)
+          and then (Mem (Result, K) and then Get (Result, K) = E
+            and then (for all K of M => Mem (Result, K)
+                 and then Get (Result, K) = Get (M, K))
+            and then (for all KK of Result =>
+                        Equivalent_Keys (KK, K) or Mem (M, KK))));
+
+   function Add (M : Map; K : Key_Type; E : Element_Type) return Map with
+   --  Returns M augmented with the mapping K -> E.
+   --  Is_Add (M, K, E, Result) should be used instead of
+   --  Result = Add (M, K, E) whenever possible both for execution and for
+   --  proof.
+
+     Global => null,
+     Pre    => not Mem (M, K) and Length (M) < Count_Type'Last,
+     Post   => Length (M) + 1 = Length (Add'Result)
+               and Is_Add (M, K, E, Add'Result);
+
+   function Is_Set
+     (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
+   --  Returns True if Result is M where the element associated to K has been
+   --  replaced by E.
+
+   with
+     Global => null,
+     Post   => Is_Set'Result =
+         (Mem (M, K)
+          and then Mem (Result, K)
+          and then Get (Result, K) = E
+          and then (for all KK of M => Mem (Result, KK)
+               and then (if not Equivalent_Keys (K, KK)
+                         then Get (Result, KK) = Get (M, KK)))
+          and then (for all K of Result => Mem (M, K)));
+
+   function Set (M : Map; K : Key_Type; E : Element_Type) return Map with
+   --  Returns M where the element associated to K has been replaced by E.
+   --  Is_Set (M, K, E, Result) should be used instead of
+   --  Result = Set (M, K, E) whenever possible both for execution and for
+   --  proof.
+
+     Global => null,
+     Pre    => Mem (M, K),
+     Post   => Length (M) = Length (Set'Result)
+     and Is_Set (M, K, E, Set'Result);
+
+   ---------------------------
+   --  Iteration Primitives --
+   ---------------------------
+
+   type Private_Key is private;
+
+   function Iter_First (M : Map) return Private_Key with
+     Global => null;
+   function Iter_Has_Element (M : Map; K : Private_Key) return Boolean with
+     Global => null;
+   function Iter_Next (M : Map; K : Private_Key) return Private_Key with
+     Global => null,
+     Pre    => Iter_Has_Element (M, K);
+   function Iter_Element (M : Map; K : Private_Key) return Key_Type with
+     Global => null,
+     Pre    => Iter_Has_Element (M, K);
+   pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+private
+   pragma SPARK_Mode (Off);
+
+   function "="  (Left, Right : Key_Type) return Boolean
+                  renames Equivalent_Keys;
+
+   subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+   package Element_Containers is new Ada.Containers.Functional_Base
+     (Element_Type        => Element_Type,
+      Index_Type          => Positive_Count_Type);
+
+   package Key_Containers is new Ada.Containers.Functional_Base
+     (Element_Type        => Key_Type,
+      Index_Type          => Positive_Count_Type);
+
+   type Map is record
+      Keys     : Key_Containers.Container;
+      Elements : Element_Containers.Container;
+   end record;
+
+   type Private_Key is new Count_Type;
+
+   function Iter_First (M : Map) return Private_Key is (1);
+
+   function Iter_Has_Element (M : Map; K : Private_Key) return Boolean is
+     (Count_Type (K) in 1 .. Key_Containers.Length (M.Keys));
+
+   function Iter_Next (M : Map; K : Private_Key) return Private_Key is
+     (if K = Private_Key'Last then 0 else K + 1);
+
+   function Iter_Element (M : Map; K : Private_Key) return Key_Type is
+     (Key_Containers.Get (M.Keys, Count_Type (K)));
+end Ada.Containers.Functional_Maps;
Index: a-cofuba.adb
===================================================================
--- a-cofuba.adb	(revision 0)
+++ a-cofuba.adb	(revision 0)
@@ -0,0 +1,206 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_BASE                      --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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;
+
+package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
+
+   pragma Assertion_Policy
+      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
+
+   function To_Count (Idx : Extended_Index) return Count_Type
+   is (Count_Type
+       (Extended_Index'Pos (Idx)
+        - Extended_Index'Pos (Extended_Index'First)));
+   function To_Index (Position : Count_Type) return Extended_Index
+   is (Extended_Index'Val
+       (Position
+        + Extended_Index'Pos (Extended_Index'First)));
+   --  Conversion functions between Index_Type and Count_Type
+
+   function Find (C : Container; E : access Element_Type) return Count_Type;
+   --  Search a container C for an element equal to E.all, return the
+   --  position in the underlying array.
+
+   ---------
+   -- "=" --
+   ---------
+
+   function "=" (C1, C2 : Container) return Boolean is
+   begin
+      if C1.Elements'Length /= C2.Elements'Length then
+         return False;
+      end if;
+
+      for I in C1.Elements'Range loop
+         if C1.Elements (I).all /= C2.Elements (I).all then
+            return False;
+         end if;
+      end loop;
+      return True;
+   end "=";
+
+   ----------
+   -- "<=" --
+   ----------
+
+   function "<=" (C1, C2 : Container) return Boolean is
+   begin
+      for I in C1.Elements'Range loop
+         if Find (C2, C1.Elements (I)) = 0 then
+            return False;
+         end if;
+      end loop;
+      return True;
+   end "<=";
+
+   ---------
+   -- Add --
+   ---------
+
+   function Add (C : Container; E : Element_Type) return Container is
+   begin
+      return Container'(Elements =>
+                           new Element_Array'
+                          (C.Elements.all & new Element_Type'(E)));
+   end Add;
+
+   ----------
+   -- Find --
+   ----------
+
+   function Find (C : Container; E : access Element_Type) return Count_Type is
+   begin
+      for I in C.Elements'Range loop
+         if C.Elements (I).all = E.all then
+            return I;
+         end if;
+      end loop;
+      return 0;
+   end Find;
+
+   function Find (C : Container; E : Element_Type) return Extended_Index is
+     (To_Index (Find (C, E'Unrestricted_Access)));
+
+   ---------
+   -- Get --
+   ---------
+
+   function Get (C : Container; I : Index_Type) return Element_Type is
+     (C.Elements (To_Count (I)).all);
+
+   ------------------
+   -- Intersection --
+   ------------------
+
+   function Intersection (C1, C2 : Container) return Container is
+      A : constant Element_Array_Access :=
+        new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>);
+      P : Count_Type := 0;
+   begin
+      for I in C1.Elements'Range loop
+         if Find (C2, C1.Elements (I)) > 0 then
+            P := P + 1;
+            A (P) := C1.Elements (I);
+         end if;
+      end loop;
+      return Container'(Elements => A);
+   end Intersection;
+
+   ------------
+   -- Length --
+   ------------
+
+   function Length (C : Container) return Count_Type is
+     (C.Elements'Length);
+
+   ---------------------
+   -- Num_Overlaps --
+   ---------------------
+
+   function Num_Overlaps (C1, C2 : Container) return Count_Type is
+      P : Count_Type := 0;
+   begin
+      for I in C1.Elements'Range loop
+         if Find (C2, C1.Elements (I)) > 0 then
+            P := P + 1;
+         end if;
+      end loop;
+      return P;
+   end Num_Overlaps;
+
+   ---------
+   -- Set --
+   ---------
+
+   function Set (C : Container; I : Index_Type; E : Element_Type)
+                 return Container
+   is
+      Result : constant Container :=
+        Container'(Elements => new Element_Array'(C.Elements.all));
+   begin
+      Result.Elements (To_Count (I)) := new Element_Type'(E);
+      return Result;
+   end Set;
+
+   -----------
+   -- Union --
+   -----------
+
+   function Union (C1, C2 : Container) return Container is
+      N : constant Count_Type := Num_Overlaps (C1, C2);
+
+   begin
+      --  if C2 is completely included in C1 then return C1
+
+      if N = Length (C2) then
+         return C1;
+      end if;
+
+      --  else loop through C2 to find the remaining elements
+
+      declare
+         L : constant Count_Type := Length (C1) - N + Length (C2);
+         A : constant Element_Array_Access :=
+           new Element_Array'(C1.Elements.all & (Length (C1) + 1 .. L => <>));
+         P : Count_Type := Length (C1);
+      begin
+         for I in C2.Elements'Range loop
+            if Find (C1, C2.Elements (I)) = 0 then
+               P := P + 1;
+               A (P) := C2.Elements (I);
+            end if;
+         end loop;
+         return Container'(Elements => A);
+      end;
+   end Union;
+
+end Ada.Containers.Functional_Base;
Index: a-cofuba.ads
===================================================================
--- a-cofuba.ads	(revision 0)
+++ a-cofuba.ads	(revision 0)
@@ -0,0 +1,104 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_BASE                      --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2016-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 --
+-- 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/>.                                          --
+------------------------------------------------------------------------------
+--  Functional containers are neither controlled nor limited. This is safe as
+--  no primitives is provided to modify them.
+--  Memory allocated inside functional containers is never reclaimed.
+
+pragma Ada_2012;
+
+private generic
+   type Index_Type is (<>);
+   --  To avoid Constraint_Error being raised at runtime, Index_Type'Base
+   --  should have at least one more element at the left than Index_Type.
+
+   type Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+package Ada.Containers.Functional_Base with SPARK_Mode => Off is
+
+   subtype Extended_Index is Index_Type'Base range
+     Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
+
+   type Container is private;
+
+   function "=" (C1, C2 : Container) return Boolean;
+   --  Return True if C1 and C2 contain the same elements at the same position
+
+   function Length (C : Container) return Count_Type;
+   --  Number of elements stored in C.
+
+   function Get (C : Container; I : Index_Type) return Element_Type;
+   --  Access to the element at index I in C.
+
+   function Set (C : Container; I : Index_Type; E : Element_Type)
+                 return Container;
+   --  Return a new container which is equal to C except for the element at
+   --  index I which is set to E.
+
+   function Add (C : Container; E : Element_Type) return Container;
+   --  Return a new container which is C appended with E.
+
+   function Find (C : Container; E : Element_Type) return Extended_Index;
+   --  Return the first index for which the element stored in C is I.
+   --  If there are no such indexes, return Extended_Index'First.
+
+   --------------------
+   -- Set Operations --
+   --------------------
+
+   function "<=" (C1, C2 : Container) return Boolean;
+   --  Return True if every element of C1 is in C2
+
+   function Num_Overlaps (C1, C2 : Container) return Count_Type;
+   --  Return the number of elements that are both in
+
+   function Union (C1, C2 : Container) return Container;
+   --  Return a container which is C1 plus all the elements of C2 that are not
+   --  in C1.
+
+   function Intersection (C1, C2 : Container) return Container;
+   --  Return a container which is C1 minus all the elements that are also in
+   --  C2.
+
+private
+
+   subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+   type Element_Access is access all Element_Type;
+   type Element_Array is
+     array (Positive_Count_Type range <>) of Element_Access;
+   type Element_Array_Access is not null access Element_Array;
+   Empty_Element_Array_Access : constant Element_Array_Access :=
+     new Element_Array'(1 .. 0 => null);
+
+   type Container is record
+      Elements : Element_Array_Access := Empty_Element_Array_Access;
+   end record;
+end Ada.Containers.Functional_Base;