with SPARK.Containers.Formal.Unbounded_Vectors;
with Ada;
with Ada.Containers;

use type Ada.Containers.Count_Type;

package Dger_Pkg
  with SPARK_Mode => On
is

   type Stride_Type is record
      Value                          : Integer;
   end record;

   package Stride_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Stride_Type);

   type Matrix_Dimension_Type is record
      Value                          : Integer;
   end record;

   package Matrix_Dimension_Type_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Matrix_Dimension_Type);

   package Long_Float_Vectors is new SPARK.Containers.Formal.Unbounded_Vectors
      (Index_Type   => Natural,
       Element_Type => Long_Float);

   function X_Storage_Index
     (Logical_I : Positive;
      M         : Matrix_Dimension_Type;
      Incx      : Stride_Type) return Natural
   is
     (if Incx.Value > 0
      then (Logical_I - 1) * Incx.Value
      else (M.Value - Logical_I) * (-Incx.Value))
   with
     Ghost,
     Pre => Incx.Value /= 0
            and then M.Value >= 1
            and then Logical_I <= M.Value;

   function Y_Storage_Index
     (Logical_J : Positive;
      N         : Matrix_Dimension_Type;
      Incy      : Stride_Type) return Natural
   is
     (if Incy.Value > 0
      then (Logical_J - 1) * Incy.Value
      else (N.Value - Logical_J) * (-Incy.Value))
   with
     Ghost,
     Pre => Incy.Value /= 0
            and then N.Value >= 1
            and then Logical_J <= N.Value;

   function A_Storage_Index
     (Row_I             : Positive;
      Column_J          : Positive;
      Leading_Dimension : Matrix_Dimension_Type) return Natural
   is
     ((Column_J - 1) * Leading_Dimension.Value + (Row_I - 1))
   with
     Ghost,
     Pre => Leading_Dimension.Value >= Row_I;

   procedure Rank_One_Update
     (Number_Of_Rows    : in     Matrix_Dimension_Type;
      Number_Of_Columns : in     Matrix_Dimension_Type;
      Alpha             : in     Long_Float;
      X                 : in     Long_Float_Vectors.Vector;
      Incx              : in     Stride_Type;
      Y                 : in     Long_Float_Vectors.Vector;
      Incy              : in     Stride_Type;
      Leading_Dimension : in     Matrix_Dimension_Type;
      A                 : in out Long_Float_Vectors.Vector)
   with
     Pre  =>
       Number_Of_Rows.Value >= 0
       and then Number_Of_Columns.Value >= 0
       and then Incx.Value /= 0
       and then Incy.Value /= 0
       and then Leading_Dimension.Value
                  >= Integer'Max (1, Number_Of_Rows.Value)
       and then (Number_Of_Rows.Value = 0
                 or else Long_Float_Vectors.Length (X)
                           >= Ada.Containers.Count_Type
                                (1
                                 + (Number_Of_Rows.Value - 1)
                                   * abs Incx.Value))
       and then (Number_Of_Columns.Value = 0
                 or else Long_Float_Vectors.Length (Y)
                           >= Ada.Containers.Count_Type
                                (1
                                 + (Number_Of_Columns.Value - 1)
                                   * abs Incy.Value))
       and then Long_Float_Vectors.Length (A)
                  >= Ada.Containers.Count_Type
                       (Leading_Dimension.Value
                        * Number_Of_Columns.Value),
     Post =>
       (if Number_Of_Rows.Value = 0
          or else Number_Of_Columns.Value = 0
          or else Alpha = 0.0
        then Long_Float_Vectors."=" (A, A'Old)
        else
          Long_Float_Vectors.Length (A)
            = Long_Float_Vectors.Length (A'Old)
          and then
            (for all I in 1 .. Number_Of_Rows.Value =>
               (for all J in 1 .. Number_Of_Columns.Value =>
                  Long_Float_Vectors.Element
                    (A,
                     A_Storage_Index
                       (Positive (I), Positive (J), Leading_Dimension))
                  = Long_Float_Vectors.Element
                      (A'Old,
                       A_Storage_Index
                         (Positive (I), Positive (J), Leading_Dimension))
                    + Alpha
                      * Long_Float_Vectors.Element
                          (X,
                           X_Storage_Index
                             (Positive (I), Number_Of_Rows, Incx))
                      * Long_Float_Vectors.Element
                          (Y,
                           Y_Storage_Index
                             (Positive (J), Number_Of_Columns, Incy)))));

   procedure Report_Invalid_Argument
     (Argument_Index : in Positive)
   with
     Pre  => Argument_Index >= 1,
     Post => True;

end Dger_Pkg;