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?
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