5

我正在将我在 Dafny 中进行的一项练习翻译成 SPARK，其中可以根据递归函数验证尾递归函数。Dafny 来源（已审查，因为它可能仍用于课程）：

function Sum(n:nat):nat 
    decreases n
{ 
    if n==0 then n else n+Sum(n-1)
}

method ComputeSum(n:nat) returns (s:nat) 
    ensures s == Sum(n) 
{
    s := 0;
    // ...censored...
}

到目前为止，我在 SPARK 中得到了什么：

function Sum (n : in Natural) return Natural
is
begin
   if n = 0 then
      return n;
   else
      return n + Sum(n - 1);
   end if;
end Sum;

function ComputeSum(n : in Natural) return Natural
  with
    Post => ComputeSum'Result = Sum(n)
is
   s : Natural := 0;
begin
   -- ...censored...
   return s;
end ComputeSum;

我似乎无法弄清楚如何表达这种decreases n情况（现在我想起来可能有点奇怪......但几年前我已经为它评分了，所以我该判断谁，问题仍然是如何把它做完）。结果，我收到可能溢出和/或无限递归的警告。

我猜要添加一个前置或后置条件。试过Pre => n <= 1显然不会溢出，但我仍然收到警告。除此之外Post => Sum'Result <= n**n，警告会消失，但该条件会得到“后置条件可能失败”的警告，这是不对的，但猜测证明者无法判断。也不是我应该检查的表达式，但我似乎无法弄清楚Post我在寻找什么。可能是非常接近递归表达式的东西，但我的尝试都没有奏效。一定错过了一些语言结构......

那么，我该如何表达递归约束呢？

编辑1：

按照此 SO 答案和此 SPARK 文档部分的链接，我尝试了以下操作：

function Sum (n : in Natural) return Natural
is
  (if n = 0 then 0 else n + Sum(n - 1))
    with
      Pre => (n in 0 .. 2),
      Contract_Cases => (n = 0 => Sum'Result = 0,
                         n >= 1 => Sum'Result = n + Sum(n - 1)),
      Subprogram_Variant => (Decreases => n);

但是从 SPARK 收到这些警告：

spark.adb:32:30: medium: overflow check might fail [reason for check: result of addition must fit in a 32-bits machine integer][#0]
spark.adb:36:56: warning: call to "Sum" within its postcondition will lead to infinite recursion
4

2 回答 2

4

如果您想证明某个尾递归求和函数的结果等于某个值的给定递归求和函数的结果N，那么原则上，只定义递归函数（作为表达式函数）就足够了后置条件。然后，您只需在尾递归函数的后置条件中提及递归（表达式）函数（请注意，ensuresDafny 中的递归函数也没有后置条件 ( )）。

但是，由于 SPARK 的主要目标之一是证明不存在运行时错误，因此您必须证明不会发生溢出，因此，您确实需要递归函数的后置条件。正如@Jeffrey Carter 在评论中已经建议的那样，这种后置条件的合理选择是算术级数的显式求和公式：

Sum (N) = N * (1 + N) / 2

这个选择实际上非常有吸引力，因为有了这个公式，我们现在还可以根据用于计算一系列自然数之和的著名数学显式表达式在功能上验证递归函数本身。

不幸的是，按原样使用这个公式只会把你带到一半的地方。在 SPARK（以及 Ada）中，前置条件和后置条件是可选的可执行的（另请参见SPARK 参考指南中的RM 11.4.2和第5.11.1节），因此它们本身必须没有任何运行时错误。因此，按原样使用公式只会让您证明任何正数都不会发生溢出，直到

max N   s.t.   N * (1 + N) <= Integer'Last        <->    N = 46340

与后置条件一样，乘法也不允许溢出（注意Natural'Last= Integer'Last= 2**31 - 1）。

要解决此问题，您需要使用已在 Ada 202x 标准库中引入的大整数包（另请参阅RM A.5.6；此包已包含在 GNAT CE 2021 和 GNAT FSF 11.2 中）。大整数是无界的，使用这些整数的计算永远不会溢出。使用这些整数，可以证明任何正数都不会发生溢出，直到

max N   s.t.   N * (1 + N) / 2 <= Natural'Last    <->    N = 65535 = 2**16 - 1

下面的示例说明了这些整数在后置条件中的用法。

一些最后的笔记：

  • 该Subprogram_Variant方面只需要证明递归子程序最终将终止。必须通过向函数添加注释来明确请求此类终止证明（也显示在下面的示例中，并且如注释中 @egilhh 指出的 SPARK 文档中所讨论的那样）。但是，您的初始目的不需要该Subprogram_Variant方面：证明某些尾递归求和函数的结果等于某个给定递归求和函数的结果 value N。

  • 要编译使用新 Ada 202x 标准库中的函数的程序，请使用编译器选项-gnat2020。

  • 虽然我使用子类型来限制 的允许值范围N，但您也可以使用前提条件。这不应该有任何区别。但是，在 SPARK（以及 Ada）中，通常认为尽可能使用（子）类型来表达约束是一种最佳实践。

  • 将反例视为可能的线索而不是事实。它们可能有意义，也可能没有意义。反例是由一些求解器可选地生成的，可能没有意义。另请参阅SPARK 用户指南中的第 7.2.6 节。

主文件

with Ada.Numerics.Big_Numbers.Big_Integers;

procedure Main with SPARK_Mode is
   
   package BI renames Ada.Numerics.Big_Numbers.Big_Integers;
   use type BI.Valid_Big_Integer;
   
   --  Conversion functions.
   function To_Big (Arg : Integer) return BI.Valid_Big_Integer renames BI.To_Big_Integer;
   function To_Int (Arg : BI.Valid_Big_Integer) return Integer renames BI.To_Integer;
      
   subtype Domain is Natural range 0 .. 2**16 - 1;
   
   function Sum (N : Domain) return Natural is
     (if N = 0 then 0 else N + Sum (N - 1))
       with
         Post => Sum'Result = To_Int (To_Big (N) * (1 + To_Big (N)) / 2),
         Subprogram_Variant => (Decreases => N);
   
   --  Request a proof that Sum will terminate for all possible values of N.
   pragma Annotate (GNATprove, Terminating, Sum);
   
begin
   null;
end Main;

输出（gnatprove）

$ gnatprove -Pdefault.gpr --output=oneline --report=all --level=1 --prover=z3
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:13:13: info: subprogram "Sum" will terminate, terminating annotation has been proved
main.adb:14:30: info: overflow check proved
main.adb:14:32: info: subprogram variant proved
main.adb:14:39: info: range check proved
main.adb:16:18: info: postcondition proved
main.adb:16:31: info: range check proved
main.adb:16:53: info: predicate check proved
main.adb:16:69: info: division check proved
main.adb:16:71: info: predicate check proved
Summary logged in [...]/gnatprove.out

附录（回应评论）

因此，您可以将后置条件添加为递归函数，但这无助于证明不存在溢出；您仍然必须在函数结果上提供一些上限，以使证明者相信表达式N + Sum (N - 1)不会导致溢出。

为了检查加法过程中是否存在溢出，证明者将根据其规范考虑所有Sum可能返回的值，并查看这些值中的至少一个是否可能导致加法溢出。在后置条件中没有显式绑定的情况下，Sum可能会根据其返回类型返回 range 中的任何值Natural'Range。该范围包括Natural'Last并且该值肯定会导致溢出。因此，证明者将报告加法可能溢出。鉴于其允许的输入值，从不返回该值的事实Sum在这里无关紧要（这就是它报告可能的原因）。因此，需要更精确的返回值上限。

如果没有确切的上限，那么您通常会退回到更保守的界限，例如，在这种情况下， （或使用 SPARK 用户手册第 5.2.7 节N * N中的斐波那契示例中所示的饱和数学，但那方法确实会改变您的功能，这可能是不可取的）。

这是一个替代示例：

示例.ads

package Example with SPARK_Mode is

   subtype Domain is Natural range 0 .. 2**15;

   function Sum (N : Domain) return Natural
     with Post => 
       Sum'Result = (if N = 0 then 0 else N + Sum (N - 1)) and
       Sum'Result <= N * N;   --  conservative upper bound if the closed form
                              --  solution to the recursive function would
                              --  not exist.
end Example;

例子.adb

package body Example with SPARK_Mode is

   function Sum (N : Domain) return Natural is
   begin
      if N = 0 then
         return N;
      else
         return N + Sum (N - 1);
      end if;
   end Sum;

end Example;

输出（gnatprove）

$ gnatprove -Pdefault.gpr --output=oneline --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
example.adb:8:19: info: overflow check proved
example.adb:8:28: info: range check proved
example.ads:7:08: info: postcondition proved
example.ads:7:45: info: overflow check proved
example.ads:7:54: info: range check proved
Summary logged in [...]/gnatprove.out
于 2021-09-12T21:15:56.633 回答
2

我找到了一些有时有效的东西，我认为这足以结束标题问题：

function Sum (n : in Natural) return Natural
is
  (if n = 0 then 0 else n + Sum(n - 1))
    with
      Pre => (n in 0 .. 10), -- works with --prover=z3, not Default (CVC4)
      -- Pre => (n in 0 .. 100), -- not working - "overflow check might fail, e.g. when n = 2"
      Subprogram_Variant => (Decreases => n),
      Post => ((n = 0 and then Sum'Result = 0)
               or (n > 0 and then Sum'Result = n + Sum(n - 1)));
      -- Contract_Cases => (n = 0 => Sum'Result = 0,
      --                    n > 0 => Sum'Result = n + Sum(n - 1)); -- warning: call to "Sum" within its postcondition will lead to infinite recursion
      -- Contract_Cases => (n = 0 => Sum'Result = 0,
      --                    n > 0 => n + Sum(n - 1) = Sum'Result); -- works
      -- Contract_Cases => (n = 0 => Sum'Result = 0,
      --                    n > 0 => Sum'Result = n * (n + 1) / 2); -- works and gives good overflow counterexamples for high n, but isn't really recursive

GNAT Studio 中的命令行调用 (Ctrl+Alt+F)、--counterproof=on 和 --prover=z3 我对它的补充：

gnatprove -P%PP -j0 %X --output=oneline --ide-progress-bar --level=0 -u %fp --counterexamples=on --prover=z3

要点：

  • Subprogram_Variant => (Decreases => n)需要告诉证明者 n 每次递归调用都会减少，就像 Dafny 版本一样。
    • 类似合同的工作方式不一致，请参阅评论Contract_Cases。
  • 默认证明者 (CVC4) 失败，使用 Z3 成功。
  • 失败的反制是没有意义的。
    • n = 2呈现为 range 的反证0 .. 100，但不是0 .. 10.
    • 可能与SPARK 用户指南中提到的这一点有关：但是，请注意，由于反例始终仅使用 CVC4 证明器生成，因此它可以解释为什么该证明器无法证明该属性。
  • 需要在更改选项之间进行清理，例如 --prover。
于 2021-09-12T18:20:16.183 回答