1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FUNCTIONAL_VECTORS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2016-2018, 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 32pragma Ada_2012; 33private with Ada.Containers.Functional_Base; 34 35generic 36 type Index_Type is (<>); 37 -- To avoid Constraint_Error being raised at run time, Index_Type'Base 38 -- should have at least one more element at the low end than Index_Type. 39 40 type Element_Type (<>) is private; 41 42package Ada.Containers.Functional_Vectors with SPARK_Mode is 43 44 subtype Extended_Index is Index_Type'Base range 45 Index_Type'Pred (Index_Type'First) .. Index_Type'Last; 46 -- Index_Type with one more element at the low end of the range. 47 -- This type is never used but it forces GNATprove to check that there is 48 -- room for one more element at the low end of Index_Type. 49 50 type Sequence is private 51 with Default_Initial_Condition => Length (Sequence) = 0, 52 Iterable => (First => Iter_First, 53 Has_Element => Iter_Has_Element, 54 Next => Iter_Next, 55 Element => Get); 56 -- Sequences are empty when default initialized. 57 -- Quantification over sequences can be done using the regular 58 -- quantification over its range or directly on its elements with "for of". 59 60 ----------------------- 61 -- Basic operations -- 62 ----------------------- 63 64 -- Sequences are axiomatized using Length and Get, providing respectively 65 -- the length of a sequence and an accessor to its Nth element: 66 67 function Length (Container : Sequence) return Count_Type with 68 -- Length of a sequence 69 70 Global => null, 71 Post => 72 (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= 73 Index_Type'Pos (Index_Type'Last); 74 75 function Get 76 (Container : Sequence; 77 Position : Extended_Index) return Element_Type 78 -- Access the Element at position Position in Container 79 80 with 81 Global => null, 82 Pre => Position in Index_Type'First .. Last (Container); 83 84 function Last (Container : Sequence) return Extended_Index with 85 -- Last index of a sequence 86 87 Global => null, 88 Post => 89 Last'Result = 90 Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + 91 Length (Container)); 92 pragma Annotate (GNATprove, Inline_For_Proof, Last); 93 94 function First return Extended_Index is (Index_Type'First); 95 -- First index of a sequence 96 97 ------------------------ 98 -- Property Functions -- 99 ------------------------ 100 101 function "=" (Left : Sequence; Right : Sequence) return Boolean with 102 -- Extensional equality over sequences 103 104 Global => null, 105 Post => 106 "="'Result = 107 (Length (Left) = Length (Right) 108 and then (for all N in Index_Type'First .. Last (Left) => 109 Get (Left, N) = Get (Right, N))); 110 pragma Annotate (GNATprove, Inline_For_Proof, "="); 111 112 function "<" (Left : Sequence; Right : Sequence) return Boolean with 113 -- Left is a strict subsequence of Right 114 115 Global => null, 116 Post => 117 "<"'Result = 118 (Length (Left) < Length (Right) 119 and then (for all N in Index_Type'First .. Last (Left) => 120 Get (Left, N) = Get (Right, N))); 121 pragma Annotate (GNATprove, Inline_For_Proof, "<"); 122 123 function "<=" (Left : Sequence; Right : Sequence) return Boolean with 124 -- Left is a subsequence of Right 125 126 Global => null, 127 Post => 128 "<="'Result = 129 (Length (Left) <= Length (Right) 130 and then (for all N in Index_Type'First .. Last (Left) => 131 Get (Left, N) = Get (Right, N))); 132 pragma Annotate (GNATprove, Inline_For_Proof, "<="); 133 134 function Contains 135 (Container : Sequence; 136 Fst : Index_Type; 137 Lst : Extended_Index; 138 Item : Element_Type) return Boolean 139 -- Returns True if Item occurs in the range from Fst to Lst of Container 140 141 with 142 Global => null, 143 Pre => Lst <= Last (Container), 144 Post => 145 Contains'Result = 146 (for some I in Fst .. Lst => Get (Container, I) = Item); 147 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 148 149 function Constant_Range 150 (Container : Sequence; 151 Fst : Index_Type; 152 Lst : Extended_Index; 153 Item : Element_Type) return Boolean 154 -- Returns True if every element of the range from Fst to Lst of Container 155 -- is equal to Item. 156 157 with 158 Global => null, 159 Pre => Lst <= Last (Container), 160 Post => 161 Constant_Range'Result = 162 (for all I in Fst .. Lst => Get (Container, I) = Item); 163 pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range); 164 165 function Equal_Except 166 (Left : Sequence; 167 Right : Sequence; 168 Position : Index_Type) return Boolean 169 -- Returns True is Left and Right are the same except at position Position 170 171 with 172 Global => null, 173 Pre => Position <= Last (Left), 174 Post => 175 Equal_Except'Result = 176 (Length (Left) = Length (Right) 177 and then (for all I in Index_Type'First .. Last (Left) => 178 (if I /= Position then Get (Left, I) = Get (Right, I)))); 179 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); 180 181 function Equal_Except 182 (Left : Sequence; 183 Right : Sequence; 184 X : Index_Type; 185 Y : Index_Type) return Boolean 186 -- Returns True is Left and Right are the same except at positions X and Y 187 188 with 189 Global => null, 190 Pre => X <= Last (Left) and Y <= Last (Left), 191 Post => 192 Equal_Except'Result = 193 (Length (Left) = Length (Right) 194 and then (for all I in Index_Type'First .. Last (Left) => 195 (if I /= X and I /= Y then 196 Get (Left, I) = Get (Right, I)))); 197 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); 198 199 function Range_Equal 200 (Left : Sequence; 201 Right : Sequence; 202 Fst : Index_Type; 203 Lst : Extended_Index) return Boolean 204 -- Returns True if the ranges from Fst to Lst contain the same elements in 205 -- Left and Right. 206 207 with 208 Global => null, 209 Pre => Lst <= Last (Left) and Lst <= Last (Right), 210 Post => 211 Range_Equal'Result = 212 (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I)); 213 pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal); 214 215 function Range_Shifted 216 (Left : Sequence; 217 Right : Sequence; 218 Fst : Index_Type; 219 Lst : Extended_Index; 220 Offset : Count_Type'Base) return Boolean 221 -- Returns True if the range from Fst to Lst in Left contains the same 222 -- elements as the range from Fst + Offset to Lst + Offset in Right. 223 224 with 225 Global => null, 226 Pre => 227 Lst <= Last (Left) 228 and then 229 (if Offset < 0 then 230 Index_Type'Pos (Index_Type'Base'First) - Offset <= 231 Index_Type'Pos (Index_Type'First)) 232 and then 233 (if Fst <= Lst then 234 Offset in 235 Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. 236 (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - 237 Index_Type'Pos (Lst)), 238 Post => 239 Range_Shifted'Result = 240 ((for all I in Fst .. Lst => 241 Get (Left, I) = 242 Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) 243 and 244 (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) .. 245 Index_Type'Val (Index_Type'Pos (Lst) + Offset) 246 => 247 Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) = 248 Get (Right, I))); 249 pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted); 250 251 ---------------------------- 252 -- Construction Functions -- 253 ---------------------------- 254 255 -- For better efficiency of both proofs and execution, avoid using 256 -- construction functions in annotations and rather use property functions. 257 258 function Set 259 (Container : Sequence; 260 Position : Index_Type; 261 New_Item : Element_Type) return Sequence 262 -- Returns a new sequence which contains the same elements as Container 263 -- except for the one at position Position which is replaced by New_Item. 264 265 with 266 Global => null, 267 Pre => Position in Index_Type'First .. Last (Container), 268 Post => 269 Get (Set'Result, Position) = New_Item 270 and then Equal_Except (Container, Set'Result, Position); 271 272 function Add (Container : Sequence; New_Item : Element_Type) return Sequence 273 -- Returns a new sequence which contains the same elements as Container 274 -- plus New_Item at the end. 275 276 with 277 Global => null, 278 Pre => 279 Length (Container) < Count_Type'Last 280 and then Last (Container) < Index_Type'Last, 281 Post => 282 Length (Add'Result) = Length (Container) + 1 283 and then Get (Add'Result, Last (Add'Result)) = New_Item 284 and then Container <= Add'Result; 285 286 function Add 287 (Container : Sequence; 288 Position : Index_Type; 289 New_Item : Element_Type) return Sequence 290 with 291 -- Returns a new sequence which contains the same elements as Container 292 -- except that New_Item has been inserted at position Position. 293 294 Global => null, 295 Pre => 296 Length (Container) < Count_Type'Last 297 and then Last (Container) < Index_Type'Last 298 and then Position <= Extended_Index'Succ (Last (Container)), 299 Post => 300 Length (Add'Result) = Length (Container) + 1 301 and then Get (Add'Result, Position) = New_Item 302 and then Range_Equal 303 (Left => Container, 304 Right => Add'Result, 305 Fst => Index_Type'First, 306 Lst => Index_Type'Pred (Position)) 307 and then Range_Shifted 308 (Left => Container, 309 Right => Add'Result, 310 Fst => Position, 311 Lst => Last (Container), 312 Offset => 1); 313 314 function Remove 315 (Container : Sequence; 316 Position : Index_Type) return Sequence 317 -- Returns a new sequence which contains the same elements as Container 318 -- except that the element at position Position has been removed. 319 320 with 321 Global => null, 322 Pre => Position in Index_Type'First .. Last (Container), 323 Post => 324 Length (Remove'Result) = Length (Container) - 1 325 and then Range_Equal 326 (Left => Container, 327 Right => Remove'Result, 328 Fst => Index_Type'First, 329 Lst => Index_Type'Pred (Position)) 330 and then Range_Shifted 331 (Left => Remove'Result, 332 Right => Container, 333 Fst => Position, 334 Lst => Last (Remove'Result), 335 Offset => 1); 336 337 --------------------------- 338 -- Iteration Primitives -- 339 --------------------------- 340 341 function Iter_First (Container : Sequence) return Extended_Index with 342 Global => null; 343 344 function Iter_Has_Element 345 (Container : Sequence; 346 Position : Extended_Index) return Boolean 347 with 348 Global => null, 349 Post => 350 Iter_Has_Element'Result = 351 (Position in Index_Type'First .. Last (Container)); 352 pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); 353 354 function Iter_Next 355 (Container : Sequence; 356 Position : Extended_Index) return Extended_Index 357 with 358 Global => null, 359 Pre => Iter_Has_Element (Container, Position); 360 361private 362 363 pragma SPARK_Mode (Off); 364 365 package Containers is new Ada.Containers.Functional_Base 366 (Index_Type => Index_Type, 367 Element_Type => Element_Type); 368 369 type Sequence is record 370 Content : Containers.Container; 371 end record; 372 373 function Iter_First (Container : Sequence) return Extended_Index is 374 (Index_Type'First); 375 376 function Iter_Next 377 (Container : Sequence; 378 Position : Extended_Index) return Extended_Index 379 is 380 (if Position = Extended_Index'Last then 381 Extended_Index'First 382 else 383 Extended_Index'Succ (Position)); 384 385 function Iter_Has_Element 386 (Container : Sequence; 387 Position : Extended_Index) return Boolean 388 is 389 (Position in Index_Type'First .. 390 (Index_Type'Val 391 ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); 392 393end Ada.Containers.Functional_Vectors; 394