1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-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-- This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada 33-- 2012 RM. The modifications are meant to facilitate formal proofs by making 34-- it easier to express properties, and by making the specification of this 35-- unit compatible with SPARK 2014. Note that the API of this unit may be 36-- subject to incompatible changes as SPARK 2014 evolves. 37 38generic 39 type Index_Type is range <>; 40 type Element_Type is private; 41 42 with function "=" (Left, Right : Element_Type) return Boolean is <>; 43 44 Bounded : Boolean := True; 45 -- If True, the containers are bounded; the initial capacity is the maximum 46 -- size, and heap allocation will be avoided. If False, the containers can 47 -- grow via heap allocation. 48 49package Ada.Containers.Formal_Vectors with 50 SPARK_Mode 51is 52 pragma Annotate (GNATprove, External_Axiomatization); 53 54 subtype Extended_Index is Index_Type'Base 55 range Index_Type'First - 1 .. 56 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; 57 58 No_Index : constant Extended_Index := Extended_Index'First; 59 60 subtype Capacity_Range is 61 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); 62 63 type Vector (Capacity : Capacity_Range) is limited private with 64 Default_Initial_Condition => Is_Empty (Vector); 65 -- In the bounded case, Capacity is the capacity of the container, which 66 -- never changes. In the unbounded case, Capacity is the initial capacity 67 -- of the container, and operations such as Reserve_Capacity and Append can 68 -- increase the capacity. The capacity never shrinks, except in the case of 69 -- Clear. 70 -- 71 -- Note that all objects of type Vector are constrained, including in the 72 -- unbounded case; you can't assign from one object to another if the 73 -- Capacity is different. 74 75 function Empty_Vector return Vector; 76 77 function "=" (Left, Right : Vector) return Boolean with 78 Global => null; 79 80 function To_Vector 81 (New_Item : Element_Type; 82 Length : Capacity_Range) return Vector 83 with 84 Global => null; 85 86 function Capacity (Container : Vector) return Capacity_Range with 87 Global => null, 88 Post => Capacity'Result >= Container.Capacity; 89 90 procedure Reserve_Capacity 91 (Container : in out Vector; 92 Capacity : Capacity_Range) 93 with 94 Global => null, 95 Pre => (if Bounded then Capacity <= Container.Capacity); 96 97 function Length (Container : Vector) return Capacity_Range with 98 Global => null; 99 100 function Is_Empty (Container : Vector) return Boolean with 101 Global => null; 102 103 procedure Clear (Container : in out Vector) with 104 Global => null; 105 -- Note that this reclaims storage in the unbounded case. You need to call 106 -- this before a container goes out of scope in order to avoid storage 107 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. 108 109 procedure Assign (Target : in out Vector; Source : Vector) with 110 Global => null, 111 Pre => (if Bounded then Length (Source) <= Target.Capacity); 112 113 function Copy 114 (Source : Vector; 115 Capacity : Capacity_Range := 0) return Vector 116 with 117 Global => null, 118 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); 119 120 function Element 121 (Container : Vector; 122 Index : Index_Type) return Element_Type 123 with 124 Global => null, 125 Pre => Index in First_Index (Container) .. Last_Index (Container); 126 127 procedure Replace_Element 128 (Container : in out Vector; 129 Index : Index_Type; 130 New_Item : Element_Type) 131 with 132 Global => null, 133 Pre => Index in First_Index (Container) .. Last_Index (Container); 134 135 procedure Append 136 (Container : in out Vector; 137 New_Item : Vector) 138 with 139 Global => null, 140 Pre => (if Bounded then 141 Length (Container) + Length (New_Item) <= Container.Capacity); 142 143 procedure Append 144 (Container : in out Vector; 145 New_Item : Element_Type) 146 with 147 Global => null, 148 Pre => (if Bounded then 149 Length (Container) < Container.Capacity); 150 151 procedure Delete_Last 152 (Container : in out Vector) 153 with 154 Global => null; 155 156 procedure Reverse_Elements (Container : in out Vector) with 157 Global => null; 158 159 procedure Swap (Container : in out Vector; I, J : Index_Type) with 160 Global => null, 161 Pre => I in First_Index (Container) .. Last_Index (Container) 162 and then J in First_Index (Container) .. Last_Index (Container); 163 164 function First_Index (Container : Vector) return Index_Type with 165 Global => null; 166 167 function First_Element (Container : Vector) return Element_Type with 168 Global => null, 169 Pre => not Is_Empty (Container); 170 171 function Last_Index (Container : Vector) return Extended_Index with 172 Global => null; 173 174 function Last_Element (Container : Vector) return Element_Type with 175 Global => null, 176 Pre => not Is_Empty (Container); 177 178 function Find_Index 179 (Container : Vector; 180 Item : Element_Type; 181 Index : Index_Type := Index_Type'First) return Extended_Index 182 with 183 Global => null; 184 185 function Reverse_Find_Index 186 (Container : Vector; 187 Item : Element_Type; 188 Index : Index_Type := Index_Type'Last) return Extended_Index 189 with 190 Global => null; 191 192 function Contains 193 (Container : Vector; 194 Item : Element_Type) return Boolean 195 with 196 Global => null; 197 198 function Has_Element 199 (Container : Vector; 200 Position : Extended_Index) return Boolean 201 with 202 Global => null; 203 204 generic 205 with function "<" (Left, Right : Element_Type) return Boolean is <>; 206 package Generic_Sorting 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 Pre => Current in First_Index (Container) .. Last_Index (Container); 223 224 function Current_To_Last 225 (Container : Vector; 226 Current : Index_Type) return Vector 227 with 228 Ghost, 229 Global => null, 230 Pre => Current in First_Index (Container) .. Last_Index (Container); 231 -- First_To_Previous returns a container containing all elements preceding 232 -- Current (excluded) in Container. Current_To_Last returns a container 233 -- containing all elements following Current (included) in Container. 234 -- These two new functions can be used to express invariant properties in 235 -- loops which iterate over containers. First_To_Previous returns the part 236 -- of the container already scanned and Current_To_Last the part not 237 -- scanned yet. 238 239private 240 pragma SPARK_Mode (Off); 241 242 pragma Inline (First_Index); 243 pragma Inline (Last_Index); 244 pragma Inline (Element); 245 pragma Inline (First_Element); 246 pragma Inline (Last_Element); 247 pragma Inline (Replace_Element); 248 pragma Inline (Contains); 249 250 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; 251 type Elements_Array is array (Array_Index range <>) of Element_Type; 252 function "=" (L, R : Elements_Array) return Boolean is abstract; 253 254 type Elements_Array_Ptr is access all Elements_Array; 255 256 type Vector (Capacity : Capacity_Range) is limited record 257 -- In the bounded case, the elements are stored in Elements. In the 258 -- unbounded case, the elements are initially stored in Elements, until 259 -- we run out of room, then we switch to Elements_Ptr. 260 Last : Extended_Index := No_Index; 261 Elements_Ptr : Elements_Array_Ptr := null; 262 Elements : aliased Elements_Array (1 .. Capacity); 263 end record; 264 265 -- The primary reason Vector is limited is that in the unbounded case, once 266 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will 267 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, 268 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would 269 -- allow SPARK to "prove" things that are false. We could fix that by 270 -- making Vector a controlled type, and override Adjust to make a deep 271 -- copy, but finalization is not allowed in SPARK. 272 -- 273 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not 274 -- allowed on Vectors. 275 276 function Empty_Vector return Vector is 277 ((Capacity => 0, others => <>)); 278 279end Ada.Containers.Formal_Vectors; 280