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

use type Ada.Containers.Count_Type;

package Dnrm2_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
      Value                          : Integer;
   end record;

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

   function Selected_Value
     (X         : Vector_Element_Type_Vectors.Vector;
      N         : Integer;
      Increment : Stride_Type;
      I         : Positive) return Float
   with Ghost,
        Pre => N > 0
               and then I <= N
               and then Natural (Vector_Element_Type_Vectors.Length (X)) >=
                          1 + (N - 1) * abs Increment.Value;

   function Sum_Of_Squares
     (X         : Vector_Element_Type_Vectors.Vector;
      N         : Integer;
      Increment : Stride_Type;
      K         : Natural) return Float
   with Ghost,
        Pre => N > 0
               and then K <= N
               and then Natural (Vector_Element_Type_Vectors.Length (X)) >=
                          1 + (N - 1) * abs Increment.Value;

   function Euclidean_Norm
     (N         : Integer;
      X         : Vector_Element_Type_Vectors.Vector;
      Increment : Stride_Type) return Vector_Element_Type
   with Pre  => (if N > 0 then
                   Natural (Vector_Element_Type_Vectors.Length (X)) >=
                     1 + (N - 1) * abs Increment.Value),
        Post => Euclidean_Norm'Result.Value >= 0.0
                and then (if N <= 0 then
                            Euclidean_Norm'Result.Value = 0.0)
                and then (if N > 0 then
                            Euclidean_Norm'Result.Value *
                            Euclidean_Norm'Result.Value =
                              Sum_Of_Squares (X, N, Increment, N))
                and then (if N > 0 and then Increment.Value = 0 then
                            Euclidean_Norm'Result.Value *
                            Euclidean_Norm'Result.Value =
                              Selected_Value (X, N, Increment, 1) *
                              Selected_Value (X, N, Increment, 1) *
                              Float (N));

end Dnrm2_Pkg;