我想找到具有以下规范的值的最小因子
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;
我编写了程序的主体,尝试涵盖所有断言,但总是有一个后置条件失败...
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 ;
我做错了什么?有人可以帮助我完成规范中的所有断言吗?
最佳答案
我不确定你所说的后置条件N'Old/Factor = N
是什么意思,但是下面显示的子程序Smallest_Factor
(也可以写成作为纯函数)在 GNAT CE 2018 中证明,可能会帮助您:
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;
与 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;
小测试运行:
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;
显示
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
关于ada - 求一个数的因数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/55191018/