package body Daxpy_Pkg
  with SPARK_Mode => On
is

   procedure Daxpy
     (N     : Integer;
      Alpha : Float;
      X     : Vector_Element_Type_Vectors.Vector;
      Inc_X : Stride_Type;
      Y     : in out Vector_Element_Type_Vectors.Vector;
      Inc_Y : Stride_Type)
   is
      use Vector_Element_Type_Vectors;

      Original_Length : constant Ada.Containers.Count_Type := Length (Y);

      IX, IY : Natural;
      Y_Elem : Vector_Element_Type;
   begin
      if N <= 0 or else Alpha = 0.0 then
         return;
      end if;

      for I in 1 .. N loop
         if Inc_X.Step > 0 then
            IX := (I - 1) * Inc_X.Step;
         else
            IX := (I - N) * Inc_X.Step;
         end if;

         if Inc_Y.Step > 0 then
            IY := (I - 1) * Inc_Y.Step;
         else
            IY := (I - N) * Inc_Y.Step;
         end if;

         Y_Elem       := Element (Y, IY);
         Y_Elem.Value := Y_Elem.Value + Alpha * Element (X, IX).Value;
         Replace_Element (Y, IY, Y_Elem);

         pragma Loop_Invariant (Length (Y) = Original_Length);
      end loop;
   end Daxpy;

end Daxpy_Pkg;