Find factor of a number

Question

I want to find the smallest factor of a value with below specification

procedure S_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)
       is

    begin
    ... 
    end S_Factor;

I wrote the body of the procedure try to cover all assert but always one of post condictions fail...

procedure S_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)
   is


begin

      Factor := N;
      for J in 2 .. Factor loop
         if N rem J /= 0  then
         null;
         else
              Factor := J;
              N := N / Factor;

            exit;
               end if;

   end loop;

end S_Factor ;

What i am doing wrong? Can someone help me past through all assert from specification?

Do you need to use *and then* instead of *and* to ensure short circuit functionality? I am not as familiar with SPARK, but in Ada you do. — Jere, Mar 15 '19 at 23:28
@Jere, @john-perry and I found that `and then` caused trouble with conditions on protected subprograms. — Simon Wright, Mar 16 '19 at 12:22
@SimonWright Was it a bug or something implementation defined? I've not done a lot of complex post conditions so this topic is interesting (or if there is a link to the issue, that is fine too, whatever is easier on you). — Jere, Mar 16 '19 at 13:41
@Jere, `and then` means that one side or the other may not get evaluated; this falls foul of the last sentence of [ARM 6.1.1(27)](http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-6-1-1.html#p27), "The prefix of an Old attribute_reference that is potentially unevaluated shall statically denote an entity" (no, I don’t understand that either :-) — Simon Wright, Mar 16 '19 at 16:01

DeeDee · Accepted Answer · 2019-03-16T12:50:05.057

I'm not sure what you mean by the post condition N'Old / Factor = N, but the subprogram Smallest_Factor shown below (which could also have been written as a pure function) proves in GNAT CE 2018 and might help you:

package Foo with SPARK_Mode is

   procedure Smallest_Factor
     (Number : in     Positive;
      Factor :    out Positive)
     with
       Pre  => (Number > 1),
       Post => (Factor in 2 .. Number)
          and then (Number rem Factor = 0)
          and then (for all J in 2 .. Factor - 1 => Number rem J /= 0);

end Foo;

with body

package body Foo with SPARK_Mode is

   procedure Smallest_Factor
     (Number : in     Positive;
      Factor :    out Positive)
   is
   begin

      Factor := 2;
      while (Number rem Factor) /= 0 loop

         pragma Loop_Invariant
           (Factor < Number);

         pragma Loop_Invariant
           (for all J in 2 .. Factor => (Number rem J) /= 0);

         Factor := Factor + 1;

      end loop;

   end Smallest_Factor;

end Foo;

A small test run:

with Ada.Text_IO;         use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;

with Foo;

procedure Main is
   Factor : Positive;
begin
   for Number in 2 .. 20 loop

      Foo.Smallest_Factor (Number, Factor);

      Put (" Number : "); Put (Number, 2);
      Put (" Factor : "); Put (Factor, 2);
      New_Line;

   end loop;   
end Main;

shows

 Number :  2 Factor :  2
 Number :  3 Factor :  3
 Number :  4 Factor :  2
 Number :  5 Factor :  5
 Number :  6 Factor :  2
 Number :  7 Factor :  7
 Number :  8 Factor :  2
 Number :  9 Factor :  3
 Number : 10 Factor :  2
 Number : 11 Factor : 11
 Number : 12 Factor :  2
 Number : 13 Factor : 13
 Number : 14 Factor :  2
 Number : 15 Factor :  3
 Number : 16 Factor :  2
 Number : 17 Factor : 17
 Number : 18 Factor :  2
 Number : 19 Factor : 19
 Number : 20 Factor :  2

Nice! I found it didn’t need the `and then` in the `while` line, or the first loop invariant. I suppose having a loop with an early exit makes it as tricky for gnatprove to reason about as it is for a human. — Simon Wright, Mar 16 '19 at 12:19
@SimonWright - Yes, you're correct! I think that an (implicit) post condition on the ```rem``` operator already proves the loop invariant ```Factor < Number```. In that case, an explicit loop condition that bounds ```Factor``` is not required. I updated the code and also slightly updated to the post condition: the range of ```Factor``` should also be bounded from above. The largest possible value for ```Factor``` is ```Number``` (when ```Number``` is prime). Thanks! — DeeDee, Mar 16 '19 at 13:02
Thank you it really help. I add N := N / Factor; on the end program because my program need it too to pass (N'Old / Factor = N) and — PoliteMan, Mar 16 '19 at 15:46

score 2 · Answer 2 · answered Mar 23 '19 at 11:37

It's a good idea to use the type system as much as possible to enforce pre- and postconditions. Simplifying your example to

package Factoring with SPARK_Mode is
   subtype Includes_Primes is Integer range 2 .. Integer'Last;

   procedure S_Factor (N : in out Includes_Primes; Factor : out Includes_Primes) with
      Post => N'Old / Factor = N and
      N'Old rem Factor = 0 and
      (for all J in 2 .. Factor - 1 => N'Old rem J /= 0);

end Factoring;

package body Factoring is
   procedure S_Factor (N : in out Includes_Primes; Factor : out Includes_Primes) is
      -- Empty
   begin -- S_Factor
      Search : for I in 2 .. N loop
         if N rem I = 0 then
            Factor := I;
            N := N / 1;

            return;
         end if;
      end loop Search;
   end S_Factor;
end Factoring;

results in the postcondition being proven automatically.

Find factor of a number

2 Answers2