package body Ddot_Pkg
  with SPARK_Mode => On
is

   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
   is
      Result : Float := 0.0;
      Ix     : Integer;
      Iy     : Integer;
   begin
      if N.Value <= 0 then
         return 0.0;
      end if;

      if Incx.Value >= 0 then
         Ix := 0;
      else
         Ix := (N.Value - 1) * abs Incx.Value;
      end if;

      if Incy.Value >= 0 then
         Iy := 0;
      else
         Iy := (N.Value - 1) * abs Incy.Value;
      end if;

      for I in 1 .. N.Value loop
         pragma Loop_Invariant (Ix >= 0);
         pragma Loop_Invariant (Iy >= 0);
         pragma Loop_Invariant
           (Ada.Containers.Count_Type (Ix)
              < Vector_Element_Type_Vectors.Length (X));
         pragma Loop_Invariant
           (Ada.Containers.Count_Type (Iy)
              < Vector_Element_Type_Vectors.Length (Y));

         Result := Result
                 + Vector_Element_Type_Vectors.Element (X, Ix).Value
                 * Vector_Element_Type_Vectors.Element (Y, Iy).Value;

         exit when I = N.Value;

         Ix := Ix + Incx.Value;
         Iy := Iy + Incy.Value;
      end loop;

      return Result;
   end Dot_Product;

end Ddot_Pkg;