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

use type Ada.Containers.Count_Type;

package Daxpy_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
      Step                           : Integer;
   end record;

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

   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)
   with
     Pre  =>
       (if N > 1 then Inc_X.Step /= 0 and then Inc_Y.Step /= 0)
       and then
         (if N > 0 then
            Vector_Element_Type_Vectors.Length (X) >=
              Ada.Containers.Count_Type (1 + (N - 1) * abs Inc_X.Step)
            and then
            Vector_Element_Type_Vectors.Length (Y) >=
              Ada.Containers.Count_Type (1 + (N - 1) * abs Inc_Y.Step)),
     Post =>
       Vector_Element_Type_Vectors.Length (Y) =
         Vector_Element_Type_Vectors.Length (Y'Old)
       and then
         (if N <= 0 or else Alpha = 0.0 then
            (for all K in 0 .. Natural (Vector_Element_Type_Vectors.Length (Y)) - 1 =>
               Vector_Element_Type_Vectors.Element (Y, K) =
               Vector_Element_Type_Vectors.Element (Y'Old, K))
          else
            (for all I in 1 .. N =>
               Vector_Element_Type_Vectors.Element
                 (Y,
                  (if Inc_Y.Step > 0 then (I - 1) * Inc_Y.Step
                   else (I - N) * Inc_Y.Step)).Value
               =
               Vector_Element_Type_Vectors.Element
                 (Y'Old,
                  (if Inc_Y.Step > 0 then (I - 1) * Inc_Y.Step
                   else (I - N) * Inc_Y.Step)).Value
               + Alpha *
                 Vector_Element_Type_Vectors.Element
                   (X,
                    (if Inc_X.Step > 0 then (I - 1) * Inc_X.Step
                     else (I - N) * Inc_X.Step)).Value));

end Daxpy_Pkg;