package body Dscal_Pkg
  with SPARK_Mode => On
is

   procedure Scale_Vector
     (Element_Count : Integer;
      Alpha         : Float;
      Vector        : in out Float_Vectors.Vector;
      Increment     : Integer)
   is
   begin
      if Element_Count <= 0 or else Increment <= 0 or else Alpha = 1.0 then
         return;
      end if;

      for K in 1 .. Element_Count loop
         declare
            Idx : constant Integer := 1 + (K - 1) * Increment;
         begin
            Float_Vectors.Replace_Element
              (Vector,
               Idx,
               Alpha * Float_Vectors.Element (Vector, Idx));
         end;

         pragma Loop_Invariant
           (Float_Vectors.Length (Vector) =
              Float_Vectors.Length (Vector'Loop_Entry));
         pragma Loop_Invariant
           (for all KK in 1 .. K =>
              Float_Vectors.Element (Vector, 1 + (KK - 1) * Increment) =
              Alpha *
              Float_Vectors.Element
                (Vector'Loop_Entry, 1 + (KK - 1) * Increment));
         pragma Loop_Invariant
           (for all I in 1 .. Integer (Float_Vectors.Length (Vector)) =>
              (if (for all KK in 1 .. K =>
                     I /= 1 + (KK - 1) * Increment)
               then
                  Float_Vectors.Element (Vector, I) =
                  Float_Vectors.Element (Vector'Loop_Entry, I)));
      end loop;
   end Scale_Vector;

end Dscal_Pkg;