And*_*eas 5 recursion ada dafny spark-2014
我正在将我在 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
如果你想证明某个尾递归求和函数的结果等于给定递归求和函数对某个值的结果N，那么原则上，只定义递归函数（作为表达式函数）就足够了，而不需要任何后置条件。ensures然后，您只需在尾递归函数的后置条件中提及递归（表达式）函数即可（请注意， Dafny 中的递归函数也没有后置条件 ( )）。
然而，由于 SPARK 的主要目标之一是证明不存在运行时错误，因此您必须证明不会发生溢出，因此，您确实需要在递归函数上添加后置条件。正如 @Jeffrey Carter 在评论中已经建议的那样，这种后置条件的合理选择是算术级数的显式求和公式：
\nSum (N) = N * (1 + N) / 2\n这个选择实际上非常有吸引力，因为使用这个公式，我们现在还可以根据众所周知的数学显式表达式来功能验证递归函数本身，以计算一系列自然数的总和。
\n不幸的是，按原样使用这个公式只会让你走到一半。在 SPARK（以及 Ada）中，前置条件和后置条件是可选可执行的（另请参阅SPARK 参考指南中的RM 11.4.2和第5.11.1节），因此它们本身必须没有任何运行时错误。因此，按原样使用公式只能让您证明任何正数都不会发生溢出，直到
\nmax N s.t. N * (1 + N) <= Integer\'Last <-> N = 46340\n与后置条件一样，乘法也不允许溢出（请注意== Natural\'Last）。Integer\'Last2**31 - 1
要解决此问题，您需要使用 Ada 202x 标准库中引入的大整数包（另请参阅RM A.5.6；该包已包含在 GNAT CE 2021 和 GNAT FSF 11.2 中） 。大整数是无界的，并且使用这些整数的计算永远不会溢出。使用这些整数，可以证明任何正数都不会发生溢出，直到
\nmax N s.t. N * (1 + N) / 2 <= Natural\'Last <-> N = 65535 = 2**16 - 1\n下面的示例说明了这些整数在后置条件中的用法。
\n最后一些注意事项：
\n该Subprogram_Variant方面仅需要证明递归子程序最终会终止。必须通过向函数添加注释来显式请求此类终止证明（也在下面的示例中显示，并且如 @egilhh 在评论中指出的 SPARK 文档中所讨论的那样）。Subprogram_Variant但是，对于您的初始目的来说，不需要该方面：证明某些尾递归求和函数的结果等于给定递归求和函数对于某个 value 的结果N。
要编译使用新 Ada 202x 标准库中的函数的程序，请使用编译器选项-gnat2020。
虽然我使用子类型来限制 的允许值范围N，但您也可以使用前提条件。这应该没有什么区别。然而，在 SPARK（以及 Ada）中，通常认为尽可能使用（子）类型表达约束是最佳实践。
将反例视为可能的线索而不是事实。它们可能有意义，也可能没有意义。反例是由某些求解器选择性生成的，可能没有意义。另请参阅SPARK user\xe2\x80\x99s 指南中的第 7.2.6 节。
\n主程序.adb
\nwith Ada.Numerics.Big_Numbers.Big_Integers;\n\nprocedure Main with SPARK_Mode is\n \n package BI renames Ada.Numerics.Big_Numbers.Big_Integers;\n use type BI.Valid_Big_Integer;\n \n -- Conversion functions.\n function To_Big (Arg : Integer) return BI.Valid_Big_Integer renames BI.To_Big_Integer;\n function To_Int (Arg : BI.Valid_Big_Integer) return Integer renames BI.To_Integer;\n \n subtype Domain is Natural range 0 .. 2**16 - 1;\n \n function Sum (N : Domain) return Natural is\n (if N = 0 then 0 else N + Sum (N - 1))\n with\n Post => Sum\'Result = To_Int (To_Big (N) * (1 + To_Big (N)) / 2),\n Subprogram_Variant => (Decreases => N);\n \n -- Request a proof that Sum will terminate for all possible values of N.\n pragma Annotate (GNATprove, Terminating, Sum);\n \nbegin\n null;\nend Main;\n输出（小虫证明）
\n$ gnatprove -Pdefault.gpr --output=oneline --report=all --level=1 --prover=z3\nPhase 1 of 2: generation of Global contracts ...\nPhase 2 of 2: flow analysis and proof ...\nmain.adb:13:13: info: subprogram "Sum" will terminate, terminating annotation has been proved\nmain.adb:14:30: info: overflow check proved\nmain.adb:14:32: info: subprogram variant proved\nmain.adb:14:39: info: range check proved\nmain.adb:16:18: info: postcondition proved\nmain.adb:16:31: info: range check proved\nmain.adb:16:53: info: predicate check proved\nmain.adb:16:69: info: division check proved\nmain.adb:16:71: info: predicate check proved\nSummary logged in [...]/gnatprove.out\n附录（回应评论）
\n因此，您可以将后置条件添加为递归函数，但这无助于证明不存在溢出；您仍然需要提供函数结果的一些上限，以使证明者相信该表达式N + Sum (N - 1)不会导致溢出。
为了检查加法过程中是否存在溢出，证明者将考虑Sum根据其规范可能返回的所有可能值，并查看这些值中是否至少有一个可能导致加法溢出。如果后置条件中没有显式绑定，Sum则可能根据其返回类型返回 range 中的任何值Natural\'Range。该范围包括Natural\'Last并且该值肯定会导致溢出。因此，证明者将报告添加可能溢出。Sum考虑到其允许的输入值，从不返回该值的事实在这里是无关紧要的（这就是它报告might的原因）。因此，需要更精确的返回值上限。
如果没有确切的上限，那么您通常会回退到更保守的界限，例如在本例中N * N（或者使用饱和数学，如 SPARK 用户手册第 5.2.7 节中的斐波那契示例所示，但是这种方法确实会改变你的功能，这可能是不可取的）。
这是一个替代示例：
\n示例.ads
\npackage Example with SPARK_Mode is\n\n subtype Domain is Natural range 0 .. 2**15;\n\n function Sum (N : Domain) return Natural\n with Post => \n Sum\'Result = (if N = 0 then 0 else N + Sum (N - 1)) and\n Sum\'Result <= N * N; -- conservative upper bound if the closed form\n -- solution to the recursive function would\n -- not exist.\nend Example;\n示例.adb
\npackage body Example with SPARK_Mode is\n\n function Sum (N : Domain) return Natural is\n begin\n if N = 0 then\n return N;\n else\n return N + Sum (N - 1);\n end if;\n end Sum;\n\nend Example;\n输出（小虫证明）
\n$ gnatprove -Pdefault.gpr --output=oneline --report=all\nPhase 1 of 2: generation of Global contracts ...\nPhase 2 of 2: flow analysis and proof ...\nexample.adb:8:19: info: overflow check proved\nexample.adb:8:28: info: range check proved\nexample.ads:7:08: info: postcondition proved\nexample.ads:7:45: info: overflow check proved\nexample.ads:7:54: info: range check proved\nSummary logged in [...]/gnatprove.out\n