1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2014-2015, Free Software Foundation, Inc. -- 10-- -- 11-- This specification is derived from the Ada Reference Manual for use with -- 12-- GNAT. The copyright notice above, and the license provisions that follow -- 13-- apply solely to the contents of the part following the private keyword. -- 14-- -- 15-- GNAT is free software; you can redistribute it and/or modify it under -- 16-- terms of the GNU General Public License as published by the Free Soft- -- 17-- ware Foundation; either version 3, or (at your option) any later ver- -- 18-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 19-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 20-- or FITNESS FOR A PARTICULAR PURPOSE. -- 21-- -- 22-- As a special exception under Section 7 of GPL version 3, you are granted -- 23-- additional permissions described in the GCC Runtime Library Exception, -- 24-- version 3.1, as published by the Free Software Foundation. -- 25-- -- 26-- You should have received a copy of the GNU General Public License and -- 27-- a copy of the GCC Runtime Library Exception along with this program; -- 28-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 29-- <http://www.gnu.org/licenses/>. -- 30------------------------------------------------------------------------------ 31 32-- Similar to Ada.Containers.Formal_Vectors. The main difference is that 33-- Element_Type may be indefinite (but not an unconstrained array). In 34-- addition, this is simplified by removing less-used functionality. 35 36with Ada.Containers.Bounded_Holders; 37with Ada.Containers.Formal_Vectors; 38 39generic 40 type Index_Type is range <>; 41 type Element_Type (<>) is private; 42 Max_Size_In_Storage_Elements : Natural := 43 Element_Type'Max_Size_In_Storage_Elements; 44 -- Maximum size of Vector elements in bytes. This has the same meaning as 45 -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that 46 -- setting this too small can lead to erroneous execution; see comments in 47 -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the 48 -- responsibility of clients to calculate the maximum size of all types in 49 -- the class. 50 51 with function "=" (Left, Right : Element_Type) return Boolean is <>; 52 53 Bounded : Boolean := True; 54 -- If True, the containers are bounded; the initial capacity is the maximum 55 -- size, and heap allocation will be avoided. If False, the containers can 56 -- grow via heap allocation. 57 58package Ada.Containers.Formal_Indefinite_Vectors with 59 SPARK_Mode => On 60is 61 pragma Annotate (GNATprove, External_Axiomatization); 62 pragma Annotate (CodePeer, Skip_Analysis); 63 64 subtype Extended_Index is Index_Type'Base 65 range Index_Type'First - 1 .. 66 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; 67 68 No_Index : constant Extended_Index := Extended_Index'First; 69 70 subtype Capacity_Range is 71 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); 72 73 type Vector (Capacity : Capacity_Range) is limited private with 74 Default_Initial_Condition; 75 76 function Empty_Vector return Vector; 77 78 function "=" (Left, Right : Vector) return Boolean with 79 Global => null; 80 81 function To_Vector 82 (New_Item : Element_Type; 83 Length : Capacity_Range) return Vector 84 with 85 Global => null; 86 87 function Capacity (Container : Vector) return Capacity_Range with 88 Global => null, 89 Post => Capacity'Result >= Container.Capacity; 90 91 procedure Reserve_Capacity 92 (Container : in out Vector; 93 Capacity : Capacity_Range) 94 with 95 Global => null, 96 Pre => (if Bounded then Capacity <= Container.Capacity); 97 98 function Length (Container : Vector) return Capacity_Range with 99 Global => null; 100 101 function Is_Empty (Container : Vector) return Boolean with 102 Global => null; 103 104 procedure Clear (Container : in out Vector) with 105 Global => null; 106 -- Note that this reclaims storage in the unbounded case. You need to call 107 -- this before a container goes out of scope in order to avoid storage 108 -- leaks. 109 110 procedure Assign (Target : in out Vector; Source : Vector) with 111 Global => null, 112 Pre => (if Bounded then Length (Source) <= Target.Capacity); 113 114 function Copy 115 (Source : Vector; 116 Capacity : Capacity_Range := 0) return Vector 117 with 118 Global => null, 119 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); 120 121 function Element 122 (Container : Vector; 123 Index : Index_Type) return Element_Type 124 with 125 Global => null, 126 Pre => Index in First_Index (Container) .. Last_Index (Container); 127 128 procedure Replace_Element 129 (Container : in out Vector; 130 Index : Index_Type; 131 New_Item : Element_Type) 132 with 133 Global => null, 134 Pre => Index in First_Index (Container) .. Last_Index (Container); 135 136 procedure Append 137 (Container : in out Vector; 138 New_Item : Vector) 139 with 140 Global => null, 141 Pre => (if Bounded 142 then Length (Container) + Length (New_Item) <= 143 Container.Capacity); 144 145 procedure Append 146 (Container : in out Vector; 147 New_Item : Element_Type) 148 with 149 Global => null, 150 Pre => (if Bounded 151 then Length (Container) < Container.Capacity); 152 153 procedure Delete_Last 154 (Container : in out Vector) 155 with 156 Global => null; 157 158 procedure Reverse_Elements (Container : in out Vector) with 159 Global => null; 160 161 procedure Swap (Container : in out Vector; I, J : Index_Type) with 162 Global => null, 163 Pre => I in First_Index (Container) .. Last_Index (Container) 164 and then J in First_Index (Container) .. Last_Index (Container); 165 166 function First_Index (Container : Vector) return Index_Type with 167 Global => null; 168 169 function First_Element (Container : Vector) return Element_Type with 170 Global => null, 171 Pre => not Is_Empty (Container); 172 173 function Last_Index (Container : Vector) return Extended_Index with 174 Global => null; 175 176 function Last_Element (Container : Vector) return Element_Type with 177 Global => null, 178 Pre => not Is_Empty (Container); 179 180 function Find_Index 181 (Container : Vector; 182 Item : Element_Type; 183 Index : Index_Type := Index_Type'First) return Extended_Index 184 with 185 Global => null; 186 187 function Reverse_Find_Index 188 (Container : Vector; 189 Item : Element_Type; 190 Index : Index_Type := Index_Type'Last) return Extended_Index 191 with 192 Global => null; 193 194 function Contains 195 (Container : Vector; 196 Item : Element_Type) return Boolean 197 with 198 Global => null; 199 200 function Has_Element 201 (Container : Vector; Position : Extended_Index) return Boolean with 202 Global => null; 203 204 generic 205 with function "<" (Left, Right : Element_Type) return Boolean is <>; 206 package Generic_Sorting with SPARK_Mode is 207 208 function Is_Sorted (Container : Vector) return Boolean with 209 Global => null; 210 211 procedure Sort (Container : in out Vector) with 212 Global => null; 213 214 end Generic_Sorting; 215 216 function First_To_Previous 217 (Container : Vector; 218 Current : Index_Type) return Vector 219 with 220 Ghost, 221 Global => null; 222 223 function Current_To_Last 224 (Container : Vector; 225 Current : Index_Type) return Vector 226 with 227 Ghost, 228 Global => null; 229 230private 231 pragma SPARK_Mode (Off); 232 233 pragma Inline (First_Index); 234 pragma Inline (Last_Index); 235 pragma Inline (Element); 236 pragma Inline (First_Element); 237 pragma Inline (Last_Element); 238 pragma Inline (Replace_Element); 239 pragma Inline (Contains); 240 241 -- The implementation method is to instantiate Bounded_Holders to get a 242 -- definite type for Element_Type, and then use that Holder type to 243 -- instantiate Formal_Vectors. All the operations are just wrappers. 244 245 package Holders is new Bounded_Holders 246 (Element_Type, Max_Size_In_Storage_Elements, "="); 247 use Holders; 248 249 package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded); 250 use Def; 251 252 -- ????Assert that Def subtypes have the same range 253 254 type Vector (Capacity : Capacity_Range) is limited record 255 V : Def.Vector (Capacity); 256 end record; 257 258 function Empty_Vector return Vector is 259 ((Capacity => 0, V => Def.Empty_Vector)); 260 261end Ada.Containers.Formal_Indefinite_Vectors; 262