package body Generic_Network is
   procedure Compute_Output (Input : Input_Vector_T; Network : in out Network_T) is
   begin
      for Neuron_Num in Network.Input_Layer'Range loop
         Network.Input_Layer(Neuron_Num).Output := Input(Neuron_Num)*
           Network.Input_Layer(Neuron_Num).Weight + Network.Input_Layer(Neuron_Num).Bias;
      end loop;

      for Neuron_Num in Network.Hidden_Layer'Range loop
         Network.Hidden_Layer(Neuron_Num).Output := 0.0;
         for Weight_Num in Network.Hidden_Layer(Neuron_Num).Weights'Range loop
            Network.Hidden_Layer(Neuron_Num).Output := Network.Hidden_Layer(Neuron_Num).Output +
              Network.Hidden_Layer(Neuron_Num).Weights(Weight_Num) *
              Network.Input_Layer(Weight_Num).Output;
         end loop;
         Network.Hidden_Layer(Neuron_Num).Output := Network.Hidden_Layer(Neuron_Num).Output +
           Network.Hidden_Layer(Neuron_Num).Bias;
      end loop;

     for Neuron_Num in Network.Output_Layer'Range loop
        null;
     end loop;
   end Compute_Output;
end Generic_Network;
generic
   Input_Len : Positive;
   Hidden_Layer_Len : Positive;
   Output_Layer_Len : Positive;
package Generic_Network is
   type Weight_T is delta 0.0000001 range -100.0..100.0;
   type Input_Vector_T is array (1..Input_Len) of Weight_T;

   type Hidden_Weights_T is array (1..Input_Len) of Weight_T;
   type Output_Weights_T is array (1..Hidden_Layer_Len) of Weight_T;

   type Input_Neuron_T is record
      Weight : Weight_T;
      D : Weight_T;
      Bias : Weight_T;
      Output : Weight_T;
   end record;

   type Hidden_Neuron_T is record
      Weights : Hidden_Weights_T;
      D : Weight_T;
      Bias : Weight_T;
      Output : Weight_T;
   end record;

   type Output_Neuron_T is record
      Weights : Output_Weights_T;
      D : Weight_T;
      Bias : Weight_T;
      Output : Weight_T;
   end record;

   type Input_Layer_T is array (1..Input_Len) of Input_Neuron_T;
   type Hidden_Layer_T is array (1..Hidden_Layer_Len) of Hidden_Neuron_T;
   type Output_Layer_T is array (1..Output_Layer_Len) of Output_Neuron_T;

   type Network_T is record
      Input_Layer : Input_Layer_T;
      Hidden_Layer : Hidden_Layer_T;
      Output_Layer : Output_Layer_T;
   end record;

   procedure Compute_Output (Input : Input_Vector_T; Network : in out Network_T)
     with Global => null,
     Depends => (Network =>+ Input);
end Generic_Network;

with Generic_Network;
procedure Main with SPARK_Mode => On is
   package MLP is new Generic_Network(Input_Len => 2,
                                     Hidden_Layer_Len => 2,
                                     Output_Layer_Len => 1);
begin
   null;
end Main;