gcc/ada/libgnat/s-gearop.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --       S Y S T E M . G E N E R I C _ A R R A Y _ O P E R A T I O N S      --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2006-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  Proof of this unit is only done up to silver level, i.e. absence of runtime
  33 --  errors, and only regarding runtime checks that depend on the generic part,
  34 --  ignoring runtime checks related to formal generic subprogram parameters
  35 --  in instantiations. For example, contracts do not protect against scalar
  36 --  overflows in arithmetic operations passed on as formal generic subprogram
  37 --  parameters.
  38
  39 --  Preconditions in this unit are meant mostly for analysis, but will be
  40 --  activated at runtime depending on the assertion policy for preconditions at
  41 --  the program point of instantiation. These preconditions are simply checking
  42 --  bounds, so should not impact running time.
  43
  44 package System.Generic_Array_Operations
  45   with SPARK_Mode
  46 is
  47
  48    pragma Pure (Generic_Array_Operations);
  49
  50    ---------------------
  51    -- Back_Substitute --
  52    ---------------------
  53
  54    generic
  55       type Scalar is private;
  56       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
  57       with function "-" (Left, Right : Scalar) return Scalar is <>;
  58       with function "*" (Left, Right : Scalar) return Scalar is <>;
  59       with function "/" (Left, Right : Scalar) return Scalar is <>;
  60       with function Is_Non_Zero (X : Scalar) return Boolean is <>;
  61    procedure Back_Substitute (M, N : in out Matrix)
  62    with
  63      Pre => M'First (1) = N'First (1)
  64        and then M'Last (1) = N'Last (1);
  65
  66    --------------
  67    -- Diagonal --
  68    --------------
  69
  70    generic
  71       type Scalar is private;
  72       type Vector is array (Integer range <>) of Scalar;
  73       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
  74    function Diagonal (A : Matrix) return Vector
  75    with
  76      Pre => A'First (1) < A'Last (1)
  77        and then A'First (2) < A'Last (2)
  78        and then (if A'First (1) <= 0 then
  79                    A'Last (1) < Integer'Last + A'First (1))
  80        and then (if A'First (2) <= 0 then
  81                    A'Last (2) < Integer'Last + A'First (2));
  82
  83    -----------------------
  84    -- Forward_Eliminate --
  85    -----------------------
  86
  87    --  Use elementary row operations to put square matrix M in row echolon
  88    --  form. Identical row operations are performed on matrix N, must have the
  89    --  same number of rows as M.
  90
  91    generic
  92       type Scalar is private;
  93       type Real is digits <>;
  94       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
  95       with function "abs" (Right : Scalar) return Real'Base is <>;
  96       with function "-" (Left, Right : Scalar) return Scalar is <>;
  97       with function "*" (Left, Right : Scalar) return Scalar is <>;
  98       with function "/" (Left, Right : Scalar) return Scalar is <>;
  99       Zero : Scalar;
 100       One  : Scalar;
 101    procedure Forward_Eliminate
 102      (M   : in out Matrix;
 103       N   : in out Matrix;
 104       Det : out Scalar)
 105    with
 106      Pre => M'First (1) = N'First (1)
 107        and then M'Last (1) = N'Last (1);
 108
 109    --------------------------
 110    -- Square_Matrix_Length --
 111    --------------------------
 112
 113    generic
 114       type Scalar is private;
 115       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 116    function Square_Matrix_Length (A : Matrix) return Natural
 117    with
 118      Pre => (if A'First (1) <= 0 then
 119                A'Last (1) < Integer'Last + A'First (1))
 120        and then (if A'First (2) <= 0 then
 121                    A'Last (2) < Integer'Last + A'First (2))
 122        and then A'Length (1) = A'Length (2);
 123    --  If A is non-square, raise Constraint_Error, else return its dimension
 124
 125    ----------------------------------
 126    -- Vector_Elementwise_Operation --
 127    ----------------------------------
 128
 129    generic
 130       type X_Scalar is private;
 131       type Result_Scalar is private;
 132       type X_Vector is array (Integer range <>) of X_Scalar;
 133       type Result_Vector is array (Integer range <>) of Result_Scalar;
 134       with function Operation (X : X_Scalar) return Result_Scalar;
 135    function Vector_Elementwise_Operation (X : X_Vector) return Result_Vector;
 136
 137    ----------------------------------
 138    -- Matrix_Elementwise_Operation --
 139    ----------------------------------
 140
 141    generic
 142       type X_Scalar is private;
 143       type Result_Scalar is private;
 144       type X_Matrix is array (Integer range <>, Integer range <>) of X_Scalar;
 145       type Result_Matrix is array (Integer range <>, Integer range <>)
 146         of Result_Scalar;
 147       with function Operation (X : X_Scalar) return Result_Scalar;
 148    function Matrix_Elementwise_Operation (X : X_Matrix) return Result_Matrix;
 149
 150    -----------------------------------------
 151    -- Vector_Vector_Elementwise_Operation --
 152    -----------------------------------------
 153
 154    generic
 155       type Left_Scalar is private;
 156       type Right_Scalar is private;
 157       type Result_Scalar is private;
 158       type Left_Vector is array (Integer range <>) of Left_Scalar;
 159       type Right_Vector is array (Integer range <>) of Right_Scalar;
 160       type Result_Vector is array (Integer range <>) of Result_Scalar;
 161       with function Operation
 162              (Left  : Left_Scalar;
 163               Right : Right_Scalar) return Result_Scalar;
 164    function Vector_Vector_Elementwise_Operation
 165      (Left  : Left_Vector;
 166       Right : Right_Vector) return Result_Vector
 167    with
 168      Pre => (if Left'First <= 0 then
 169                Left'Last < Integer'Last + Left'First)
 170        and then (if Right'First <= 0 then
 171                    Right'Last < Integer'Last + Right'First)
 172        and then Left'Length = Right'Length;
 173
 174    ------------------------------------------------
 175    -- Vector_Vector_Scalar_Elementwise_Operation --
 176    ------------------------------------------------
 177
 178    generic
 179       type X_Scalar is private;
 180       type Y_Scalar is private;
 181       type Z_Scalar is private;
 182       type Result_Scalar is private;
 183       type X_Vector is array (Integer range <>) of X_Scalar;
 184       type Y_Vector is array (Integer range <>) of Y_Scalar;
 185       type Result_Vector is array (Integer range <>) of Result_Scalar;
 186       with function Operation
 187              (X : X_Scalar;
 188               Y : Y_Scalar;
 189               Z : Z_Scalar) return Result_Scalar;
 190    function Vector_Vector_Scalar_Elementwise_Operation
 191      (X : X_Vector;
 192       Y : Y_Vector;
 193       Z : Z_Scalar) return Result_Vector
 194    with
 195      Pre => (if X'First <= 0 then X'Last < Integer'Last + X'First)
 196        and then (if Y'First <= 0 then Y'Last < Integer'Last + Y'First)
 197        and then X'Length = Y'Length;
 198
 199    -----------------------------------------
 200    -- Matrix_Matrix_Elementwise_Operation --
 201    -----------------------------------------
 202
 203    generic
 204       type Left_Scalar is private;
 205       type Right_Scalar is private;
 206       type Result_Scalar is private;
 207       type Left_Matrix is array (Integer range <>, Integer range <>)
 208         of Left_Scalar;
 209       type Right_Matrix is array (Integer range <>, Integer range <>)
 210         of Right_Scalar;
 211       type Result_Matrix is array (Integer range <>, Integer range <>)
 212         of Result_Scalar;
 213       with function Operation
 214              (Left  : Left_Scalar;
 215               Right : Right_Scalar) return Result_Scalar;
 216    function Matrix_Matrix_Elementwise_Operation
 217      (Left  : Left_Matrix;
 218       Right : Right_Matrix) return Result_Matrix
 219    with
 220      Pre => (if Left'First (1) <= 0 then
 221                Left'Last (1) < Integer'Last + Left'First (1))
 222        and then (if Right'First (1) <= 0 then
 223                    Right'Last (1) < Integer'Last + Right'First (1))
 224        and then Left'Length (1) = Right'Length (1)
 225        and then (if Left'First (2) <= 0 then
 226                    Left'Last (2) < Integer'Last + Left'First (2))
 227        and then (if Right'First (2) <= 0 then
 228                    Right'Last (2) < Integer'Last + Right'First (2))
 229        and then Left'Length (2) = Right'Length (2);
 230
 231    ------------------------------------------------
 232    -- Matrix_Matrix_Scalar_Elementwise_Operation --
 233    ------------------------------------------------
 234
 235    generic
 236       type X_Scalar is private;
 237       type Y_Scalar is private;
 238       type Z_Scalar is private;
 239       type Result_Scalar is private;
 240       type X_Matrix is array (Integer range <>, Integer range <>) of X_Scalar;
 241       type Y_Matrix is array (Integer range <>, Integer range <>) of Y_Scalar;
 242       type Result_Matrix is array (Integer range <>, Integer range <>)
 243         of Result_Scalar;
 244       with function Operation
 245              (X : X_Scalar;
 246               Y : Y_Scalar;
 247               Z : Z_Scalar) return Result_Scalar;
 248    function Matrix_Matrix_Scalar_Elementwise_Operation
 249      (X : X_Matrix;
 250       Y : Y_Matrix;
 251       Z : Z_Scalar) return Result_Matrix
 252    with
 253      Pre => (if X'First (1) <= 0 then
 254                X'Last (1) < Integer'Last + X'First (1))
 255        and then (if Y'First (1) <= 0 then
 256                    Y'Last (1) < Integer'Last + Y'First (1))
 257        and then X'Length (1) = Y'Length (1)
 258        and then (if X'First (2) <= 0 then
 259                    X'Last (2) < Integer'Last + X'First (2))
 260        and then (if Y'First (2) <= 0 then
 261                    Y'Last (2) < Integer'Last + Y'First (2))
 262        and then X'Length (2) = Y'Length (2);
 263
 264    -----------------------------------------
 265    -- Vector_Scalar_Elementwise_Operation --
 266    -----------------------------------------
 267
 268    generic
 269       type Left_Scalar is private;
 270       type Right_Scalar is private;
 271       type Result_Scalar is private;
 272       type Left_Vector is array (Integer range <>) of Left_Scalar;
 273       type Result_Vector is array (Integer range <>) of Result_Scalar;
 274       with function Operation
 275              (Left  : Left_Scalar;
 276               Right : Right_Scalar) return Result_Scalar;
 277    function Vector_Scalar_Elementwise_Operation
 278      (Left  : Left_Vector;
 279       Right : Right_Scalar) return Result_Vector;
 280
 281    -----------------------------------------
 282    -- Matrix_Scalar_Elementwise_Operation --
 283    -----------------------------------------
 284
 285    generic
 286       type Left_Scalar is private;
 287       type Right_Scalar is private;
 288       type Result_Scalar is private;
 289       type Left_Matrix is array (Integer range <>, Integer range <>)
 290         of Left_Scalar;
 291       type Result_Matrix is array (Integer range <>, Integer range <>)
 292         of Result_Scalar;
 293       with function Operation
 294              (Left  : Left_Scalar;
 295               Right : Right_Scalar) return Result_Scalar;
 296    function Matrix_Scalar_Elementwise_Operation
 297      (Left  : Left_Matrix;
 298       Right : Right_Scalar) return Result_Matrix;
 299
 300    -----------------------------------------
 301    -- Scalar_Vector_Elementwise_Operation --
 302    -----------------------------------------
 303
 304    generic
 305       type Left_Scalar is private;
 306       type Right_Scalar is private;
 307       type Result_Scalar is private;
 308       type Right_Vector is array (Integer range <>) of Right_Scalar;
 309       type Result_Vector is array (Integer range <>) of Result_Scalar;
 310       with function Operation
 311              (Left  : Left_Scalar;
 312               Right : Right_Scalar) return Result_Scalar;
 313    function Scalar_Vector_Elementwise_Operation
 314      (Left  : Left_Scalar;
 315       Right : Right_Vector) return Result_Vector;
 316
 317    -----------------------------------------
 318    -- Scalar_Matrix_Elementwise_Operation --
 319    -----------------------------------------
 320
 321    generic
 322       type Left_Scalar is private;
 323       type Right_Scalar is private;
 324       type Result_Scalar is private;
 325       type Right_Matrix is array (Integer range <>, Integer range <>)
 326         of Right_Scalar;
 327       type Result_Matrix is array (Integer range <>, Integer range <>)
 328         of Result_Scalar;
 329       with function Operation
 330              (Left  : Left_Scalar;
 331               Right : Right_Scalar) return Result_Scalar;
 332    function Scalar_Matrix_Elementwise_Operation
 333      (Left  : Left_Scalar;
 334       Right : Right_Matrix) return Result_Matrix;
 335
 336    -------------------
 337    -- Inner_Product --
 338    -------------------
 339
 340    generic
 341       type Left_Scalar is private;
 342       type Right_Scalar is private;
 343       type Result_Scalar is private;
 344       type Left_Vector is array (Integer range <>) of Left_Scalar;
 345       type Right_Vector is array (Integer range <>) of Right_Scalar;
 346       Zero : Result_Scalar;
 347       with function "*"
 348              (Left  : Left_Scalar;
 349               Right : Right_Scalar) return Result_Scalar is <>;
 350       with function "+"
 351              (Left  : Result_Scalar;
 352               Right : Result_Scalar) return Result_Scalar is <>;
 353    function Inner_Product
 354      (Left  : Left_Vector;
 355       Right : Right_Vector) return Result_Scalar
 356    with
 357      Pre => (if Left'First <= 0 then
 358                Left'Last < Integer'Last + Left'First)
 359        and then (if Right'First <= 0 then
 360                    Right'Last < Integer'Last + Right'First)
 361        and then Left'Length = Right'Length;
 362
 363    -------------
 364    -- L2_Norm --
 365    -------------
 366
 367    generic
 368       type X_Scalar is private;
 369       type Result_Real is digits <>;
 370       type X_Vector is array (Integer range <>) of X_Scalar;
 371       with function "abs" (Right : X_Scalar) return Result_Real is <>;
 372       with function Sqrt (X : Result_Real'Base) return Result_Real'Base is <>;
 373    function L2_Norm (X : X_Vector) return Result_Real'Base;
 374
 375    -------------------
 376    -- Outer_Product --
 377    -------------------
 378
 379    generic
 380       type Left_Scalar is private;
 381       type Right_Scalar is private;
 382       type Result_Scalar is private;
 383       type Left_Vector is array (Integer range <>) of Left_Scalar;
 384       type Right_Vector is array (Integer range <>) of Right_Scalar;
 385       type Matrix is array (Integer range <>, Integer range <>)
 386         of Result_Scalar;
 387       with function "*"
 388              (Left  : Left_Scalar;
 389               Right : Right_Scalar) return Result_Scalar is <>;
 390    function Outer_Product
 391      (Left  : Left_Vector;
 392       Right : Right_Vector) return Matrix;
 393
 394    ---------------------------
 395    -- Matrix_Vector_Product --
 396    ---------------------------
 397
 398    generic
 399       type Left_Scalar is private;
 400       type Right_Scalar is private;
 401       type Result_Scalar is private;
 402       type Matrix is array (Integer range <>, Integer range <>)
 403         of Left_Scalar;
 404       type Right_Vector is array (Integer range <>) of Right_Scalar;
 405       type Result_Vector is array (Integer range <>) of Result_Scalar;
 406       Zero : Result_Scalar;
 407       with function "*"
 408              (Left  : Left_Scalar;
 409               Right : Right_Scalar) return Result_Scalar is <>;
 410       with function "+"
 411              (Left  : Result_Scalar;
 412               Right : Result_Scalar) return Result_Scalar is <>;
 413    function Matrix_Vector_Product
 414      (Left  : Matrix;
 415       Right : Right_Vector) return Result_Vector
 416    with
 417      Pre => (if Left'First (2) <= 0 then
 418                Left'Last (2) < Integer'Last + Left'First (2))
 419        and then (if Right'First <= 0 then
 420                    Right'Last < Integer'Last + Right'First)
 421        and then Left'Length (2) = Right'Length;
 422
 423    ---------------------------
 424    -- Vector_Matrix_Product --
 425    ---------------------------
 426
 427    generic
 428       type Left_Scalar is private;
 429       type Right_Scalar is private;
 430       type Result_Scalar is private;
 431       type Left_Vector is array (Integer range <>) of Left_Scalar;
 432       type Matrix is array (Integer range <>, Integer range <>)
 433         of Right_Scalar;
 434       type Result_Vector is array (Integer range <>) of Result_Scalar;
 435       Zero : Result_Scalar;
 436       with function "*"
 437              (Left  : Left_Scalar;
 438               Right : Right_Scalar) return Result_Scalar is <>;
 439       with function "+"
 440              (Left  : Result_Scalar;
 441               Right : Result_Scalar) return Result_Scalar is <>;
 442    function Vector_Matrix_Product
 443      (Left  : Left_Vector;
 444       Right : Matrix) return Result_Vector
 445    with
 446      Pre => (if Left'First <= 0 then
 447                Left'Last < Integer'Last + Left'First)
 448        and then (if Right'First (1) <= 0 then
 449                    Right'Last (1) < Integer'Last + Right'First (1))
 450        and then Left'Length = Right'Length (1);
 451
 452    ---------------------------
 453    -- Matrix_Matrix_Product --
 454    ---------------------------
 455
 456    generic
 457       type Left_Scalar is private;
 458       type Right_Scalar is private;
 459       type Result_Scalar is private;
 460       type Left_Matrix is array (Integer range <>, Integer range <>)
 461         of Left_Scalar;
 462       type Right_Matrix is array (Integer range <>, Integer range <>)
 463         of Right_Scalar;
 464       type Result_Matrix is array (Integer range <>, Integer range <>)
 465         of Result_Scalar;
 466       Zero : Result_Scalar;
 467       with function "*"
 468              (Left  : Left_Scalar;
 469               Right : Right_Scalar) return Result_Scalar is <>;
 470       with function "+"
 471              (Left  : Result_Scalar;
 472               Right : Result_Scalar) return Result_Scalar is <>;
 473    function Matrix_Matrix_Product
 474      (Left  : Left_Matrix;
 475       Right : Right_Matrix) return Result_Matrix
 476    with
 477      Pre => (if Left'First (2) <= 0 then
 478                Left'Last (2) < Integer'Last + Left'First (2))
 479        and then (if Right'First (1) <= 0 then
 480                    Right'Last (1) < Integer'Last + Right'First (1))
 481        and then Left'Length (2) = Right'Length (1);
 482
 483    ----------------------------
 484    -- Matrix_Vector_Solution --
 485    ----------------------------
 486
 487    generic
 488       type Scalar is private;
 489       Zero : Scalar;
 490       type Vector is array (Integer range <>) of Scalar;
 491       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 492       with procedure Back_Substitute (M, N : in out Matrix) is <>;
 493       with procedure Forward_Eliminate
 494              (M   : in out Matrix;
 495               N   : in out Matrix;
 496               Det : out Scalar) is <>;
 497    function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector
 498    with
 499      Pre => (if A'First (1) <= 0 then
 500                A'Last (1) < Integer'Last + A'First (1))
 501        and then (if A'First (2) <= 0 then
 502                    A'Last (2) < Integer'Last + A'First (2))
 503        and then A'Length (1) = A'Length (2)
 504        and then (if X'First <= 0 then
 505                    X'Last < Integer'Last + X'First)
 506        and then A'Length (1) = X'Length;
 507
 508    ----------------------------
 509    -- Matrix_Matrix_Solution --
 510    ----------------------------
 511
 512    generic
 513       type Scalar is private;
 514       Zero : Scalar;
 515       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 516       with procedure Back_Substitute (M, N : in out Matrix) is <>;
 517       with procedure Forward_Eliminate
 518              (M   : in out Matrix;
 519               N   : in out Matrix;
 520               Det : out Scalar) is <>;
 521    function Matrix_Matrix_Solution (A : Matrix; X : Matrix) return Matrix
 522    with
 523      Pre => (if A'First (1) <= 0 then
 524                A'Last (1) < Integer'Last + A'First (1))
 525        and then (if A'First (2) <= 0 then
 526                    A'Last (2) < Integer'Last + A'First (2))
 527        and then A'Length (1) = A'Length (2)
 528        and then (if X'First (1) <= 0 then
 529                    X'Last (1) < Integer'Last + X'First (1))
 530        and then A'Length (1) = X'Length (1);
 531
 532    ----------
 533    -- Sqrt --
 534    ----------
 535
 536    generic
 537       type Real is digits <>;
 538    function Sqrt (X : Real'Base) return Real'Base;
 539
 540    -----------------
 541    -- Swap_Column --
 542    -----------------
 543
 544    generic
 545       type Scalar is private;
 546       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 547    procedure Swap_Column (A : in out Matrix; Left, Right : Integer)
 548    with
 549      Pre => Left in A'Range (2)
 550        and then Right in A'Range (2);
 551
 552    ---------------
 553    -- Transpose --
 554    ---------------
 555
 556    generic
 557       type Scalar is private;
 558       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 559    procedure Transpose (A : Matrix; R : out Matrix)
 560    with
 561      Relaxed_Initialization => R,
 562      Pre  => A'First (1) = R'First (2)
 563        and then A'Last (1) = R'Last (2)
 564        and then A'First (2) = R'First (1)
 565        and then A'Last (2) = R'Last (1)
 566        and then (if A'First (1) < 0 then
 567                    A'Last (1) <= Integer'Last + A'First (1))
 568        and then (if A'First (2) < 0 then
 569                    A'Last (2) <= Integer'Last + A'First (2)),
 570      Post => R'Initialized;
 571
 572    -------------------------------
 573    -- Update_Vector_With_Vector --
 574    -------------------------------
 575
 576    generic
 577       type X_Scalar is private;
 578       type Y_Scalar is private;
 579       type X_Vector is array (Integer range <>) of X_Scalar;
 580       type Y_Vector is array (Integer range <>) of Y_Scalar;
 581       with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
 582    procedure Update_Vector_With_Vector (X : in out X_Vector; Y : Y_Vector)
 583    with
 584      Pre => (if X'First <= 0 then
 585                X'Last < Integer'Last + X'First)
 586        and then (if Y'First <= 0 then
 587                    Y'Last < Integer'Last + Y'First)
 588        and then X'Length = Y'Length;
 589
 590    -------------------------------
 591    -- Update_Matrix_With_Matrix --
 592    -------------------------------
 593
 594    generic
 595       type X_Scalar is private;
 596       type Y_Scalar is private;
 597       type X_Matrix is array (Integer range <>, Integer range <>) of X_Scalar;
 598       type Y_Matrix is array (Integer range <>, Integer range <>) of Y_Scalar;
 599       with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
 600    procedure Update_Matrix_With_Matrix (X : in out X_Matrix; Y : Y_Matrix)
 601    with
 602      Pre => (if X'First (1) <= 0 then
 603                X'Last (1) < Integer'Last + X'First (1))
 604        and then (if Y'First (1) <= 0 then
 605                    Y'Last (1) < Integer'Last + Y'First (1))
 606        and then X'Length (1) = Y'Length (1)
 607        and then (if X'First (2) <= 0 then
 608                    X'Last (2) < Integer'Last + X'First (2))
 609        and then (if Y'First (2) <= 0 then
 610                    Y'Last (2) < Integer'Last + Y'First (2))
 611        and then X'Length (2) = Y'Length (2);
 612
 613    -----------------
 614    -- Unit_Matrix --
 615    -----------------
 616
 617    generic
 618       type Scalar is private;
 619       type Matrix is array (Integer range <>, Integer range <>) of Scalar;
 620       Zero : Scalar;
 621       One  : Scalar;
 622    function Unit_Matrix
 623      (Order   : Positive;
 624       First_1 : Integer := 1;
 625       First_2 : Integer := 1) return Matrix
 626    with
 627      Pre => First_1 <= Integer'Last - Order + 1
 628        and then First_2 <= Integer'Last - Order + 1;
 629
 630    -----------------
 631    -- Unit_Vector --
 632    -----------------
 633
 634    generic
 635       type Scalar is private;
 636       type Vector is array (Integer range <>) of Scalar;
 637       Zero : Scalar;
 638       One  : Scalar;
 639    function Unit_Vector
 640      (Index : Integer;
 641       Order : Positive;
 642       First : Integer := 1) return Vector
 643    with
 644      Pre => Index >= First
 645        and then First <= Integer'Last - Order + 1
 646        and then Index <= First + (Order - 1);
 647
 648 end System.Generic_Array_Operations;