找出一个数的因数答案

【问题标题】：Find factor of a number找出一个数的因数
【发布时间】：2019-03-15 21:39:49
【问题描述】：

我想找到具有以下规格的值的最小因子

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 ;

我做错了什么？有人可以帮助我通过规范中的所有断言吗？

【问题讨论】：

是否需要使用然后而不是and来确保短路功能？我对 SPARK 不太熟悉，但在 Ada 中你很熟悉。
@Jere、@john-perry 和我发现 and then 在受保护的子程序上造成了问题。
@SimonWright 是错误还是定义了某些实现？我没有做过很多复杂的发布条件，所以这个话题很有趣（或者如果有指向这个问题的链接，那也很好，不管你更容易）。
@Jere, and then 表示一侧或另一侧可能无法评估；这违反了ARM 6.1.1(27) 的最后一句话，“可能未评估的旧属性引用的前缀应静态表示一个实体”（不，我也不明白 :-)
@SimonWright 谢谢！

标签： ada formal-verification spark-ada spark-2014

【解决方案1】：

我不确定你所说的后置条件 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;

有身体

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

【讨论】：

不错！我发现它不需要while 行中的and then 或第一个循环不变量。我想有一个提前退出的循环让 gnatprove 推理和人类推理一样棘手。
@SimonWright - 是的，你是对的！我认为rem 运算符上的（隐式）后置条件已经证明了循环不变Factor < Number。在这种情况下，不需要限制Factor 的显式循环条件。我更新了代码并稍微更新了后置条件：Factor 的范围也应该从上面限定。 Factor 的最大可能值为 Number（当 Number 为素数时）。谢谢！
谢谢你的帮助。我添加 N := N / 因子；在最终程序上，因为我的程序也需要它通过 (N'Old / Factor = N) 和

【解决方案2】：

最好尽可能使用类型系统来强制执行前置条件和后置条件。将您的示例简化为

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);

结束保理；

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;

自动证明后置条件。

【讨论】：