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

use type Ada.Containers.Count_Type;

package Dscal_Pkg
  with SPARK_Mode => On
is

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

   procedure Scale_Vector
     (Element_Count : Integer;
   Alpha         : Float;
   Vector        : in out Float_Vectors.Vector;
   Increment     : Integer)
     with
    Pre  => (if Element_Count > 0 and then Increment > 0 then
               Float_Vectors.Length (Vector) >=
                 Ada.Containers.Count_Type (1 + (Element_Count - 1) * Increment)),
    Post => (if Element_Count <= 0
               or else Increment <= 0
               or else Alpha = 1.0
             then
               (for all I in 1 .. Integer (Float_Vectors.Length (Vector)) =>
                  Float_Vectors.Element (Vector, I) =
                  Float_Vectors.Element (Vector'Old, I)))
            and then
            (if Element_Count > 0
               and then Increment > 0
               and then Alpha /= 1.0
             then
               (for all K in 1 .. Element_Count =>
                  Float_Vectors.Element (Vector, 1 + (K - 1) * Increment) =
                  Alpha * Float_Vectors.Element (Vector'Old, 1 + (K - 1) * Increment))
               and then
               (for all I in 1 .. Integer (Float_Vectors.Length (Vector)) =>
                  (if (for all K in 1 .. Element_Count =>
                         I /= 1 + (K - 1) * Increment)
                   then
                      Float_Vectors.Element (Vector, I) =
                      Float_Vectors.Element (Vector'Old, I))));

end Dscal_Pkg;