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

   if N /= 2 then

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

         if N rem I = 0 then
            Factor := I;
            exit Outer_Loop;
         end if;

      end loop Outer_Loop;

   end if;

   N := N / Factor;

end Smallest_Factor;