package Factor with SPARK_Mode
is
   procedure Smallest_Factor (N : in out Positive; Factor : out Positive)
     with SPARK_Mode,
     Pre => N > 1,
     Post => (Factor > 1) and
             (N'Old / Factor = N) and
             (N'Old rem Factor = 0) and
             (for all J in 2 .. Factor - 1 => N'Old rem J /= 0);

end Factor;

-- =================================================

package body Factor with SPARK_Mode
is

   procedure Smallest_Factor (N : in out Positive; Factor : out Positive)
     with SPARK_Mode
   is
   begin
      Factor := 2;
      for I in 2 .. N loop

         pragma Loop_Invariant (for all J in 2 .. I - 1 => N rem J /= 0);

         Factor := I;
         exit when N rem I = 0;
      end loop;

      N := N / Factor;

   end Smallest_Factor;

end Factor