with Ada.Integer_Text_IO;

package body Max2 with SPARK_Mode is
   function FindMax2 (V : Vector) return Integer is
      Const : Boolean := True;
      Max1 : Integer := 0;
      Max2 : Integer := 0;
   begin
      if V'Length = 2 then
         if V(V'First) > V(V'Last) and then V(V'Last) >= 0 then return V(V'Last);
            elsif V(V'First) < V(V'Last) and then V(V'First) >= 0 then return V(V'First);
            else return 0;
         end if;
      elsif V'Length = 1 then
         return 0;
      else

         for I in Integer range V'Range loop
            pragma Loop_Invariant (Max1 >= Max2);
            pragma Loop_Invariant (Max2 >= 0);
            pragma Loop_Invariant (if const = True then (for all Index1 in V'First .. I =>
                                                           (for all Index2 in V'First .. Index1 =>
                                                              (V(Index1) = V(Index2)))));

            if I > V'First then
               if V(I) /= V(I - 1) then
                  const := False;
               end if;
            end if;

            if I = V'Last and then const = True then
               return 0;
            end if;


            if V(I) > Max1 then
               Max2 := Max1;
               Max1 := V(I);
            end if;

            if (V(I) < Max1 and V(I) > Max2) then
               Max2 := V(I);
            end if;

         end loop;
      end if;


      return Max2;
   end FindMax2;
end Max2;