package body Max with SPARK_Mode
is
function FindMax2 (V : Vector) return Integer
   is
      SecondMax : Natural := 0;
      Max : Natural := 0;
   begin

      for I in V'Range loop
         if V(I) > Max then
            SecondMax := Max;
            Max := V(I);
         elsif V(I) > SecondMax and V(I) < Max then
            SecondMax := V(I);
         end if;

         pragma Loop_Invariant (for all J in V'First .. I => V(J) <= Max);
         pragma Loop_Invariant (for some J in V'First .. I => V(J) = Max);
         pragma Loop_Invariant (if SecondMax = 0 then (for all J in V'First .. I => V(J) = Max));
         pragma Loop_Invariant (if SecondMax /= 0 then (for some  J in V'First .. I => V(J) = SecondMax));
         pragma Loop_Invariant (if SecondMax /= 0 then (for some  J in V'First .. I => V(J) > SecondMax));
         pragma Loop_Invariant (for all K in V'First .. I => (if V(K) > SecondMax then V(K) = Max));

      end loop;

      return SecondMax;
end FindMax2;


end Max;