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

use type Ada.Containers.Count_Type;

package Ddot_Pkg
  with SPARK_Mode => On
is

   type Vector_Element_Type is record
      Value                          : Float;
   end record;

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

   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 Element_Count_Type is record
      Value                          : Integer;
   end record;

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

   function Dot_Product
     (N      : Element_Count_Type;
      X      : Vector_Element_Type_Vectors.Vector;
      Incx   : Stride_Type;
      Y      : Vector_Element_Type_Vectors.Vector;
      Incy   : Stride_Type) return Float
   with
     Pre  => (if N.Value > 0 then
                Vector_Element_Type_Vectors.Length (X) >=
                  Ada.Containers.Count_Type
                    (1 + (N.Value - 1) * abs Incx.Value)
                and then
                Vector_Element_Type_Vectors.Length (Y) >=
                  Ada.Containers.Count_Type
                    (1 + (N.Value - 1) * abs Incy.Value)),
     Post => (if N.Value <= 0 then Dot_Product'Result = 0.0);

end Ddot_Pkg;