在阅读了Dafny入门：指南之后，我决定创建我的第一个程序：给定一个整数序列，计算其元素的总和。但是，我很难让Dafny验证该程序。
function G(a: seq<int>): int
decreases |a|
{
if |a| == 0 then 0 else a[0] + G(a[1..])
}
method sum(a: seq<int>) returns (r: int)
ensures r == G(a)
{
r := 0;
var i: int := 0;
while i < |a|
invariant 0 <= i <= |a|
invariant r == G(a[0..i])
{
r := r + a[i];
i := i + 1;
}
}
我得到
stdin.dfy(12,2): Error BP5003: A postcondition might not hold on this return path.
stdin.dfy(8,12): Related location: This is the postcondition that might not hold.
stdin.dfy(14,16): Error BP5005: This loop invariant might not be maintained by the loop.
我怀疑Dafny需要一些"帮助"来验证程序(也许是引理？)，但我不知道从哪里开始。
这是验证的程序版本。
有两件事需要修复：后置条件在循环之后的证明，以及循环不变性保持不变的证明。
后置条件
Dafny需要一个提示，试图证明a == a[..|a|]可能会有所帮助。断言相等足以完成这部分证明：Dafny 自动证明相等并使用它来证明循环不变量的后置条件。
这是一种常见的模式。你可以试着看看是什么困扰着Dafny，方法是在Dafny中"手工"做证明，通过做出各种断言，你将用它来在纸上向自己证明这一点。
循环不变
这个有点复杂。我们需要证明更新r和递增i可以保留r == G(a[..i])。为此，我使用了一个calc语句，让我们通过一系列中间步骤来证明相等。(如果您愿意，总是可以在没有calc的情况下证明这些事情，通过断言所有相关的等式以及calc中的任何断言。但我认为calc更好。
我将calc语句放在更新之前，r和i发生。我知道更新发生后，我需要证明r == G(a[..i])更新的r和i值。因此，在更新发生之前，足以证明未更新值r + a[i] == G(a[..i+1])。我calc声明以r + a[i]开头，并朝着G(a[..i+1])努力。
首先，通过进入循环时的循环不变性，我们知道当前值r == G(a[i])。
接下来，我们想把a[i]带到G里。这个事实并非完全微不足道，因此我们需要一个引理。我选择证明一些比必要的稍微更通用的东西，即G(a + b) == G(a) + G(b)任何整数序列a和b。我称之为引理G_append。它的证明将在下面讨论。现在，我们只是使用它来将a[i]作为单例序列带入内部。
此calc的最后一步是将a[0..i] + [a[i]]合并为a[0..i+1]。这是另一个序列外延性事实，因此需要明确断言。
这样就完成了calc，这证明了不变量是守恒的。
引理
G_append的证明通过a的归纳进行。自动处理a == []的基本情况。在归纳情况下，我们需要证明G(a + b) == G(a) + G(b)，假设a的任何子序列的归纳假设。为此，我使用了另一个calc语句。
从G(a + b)开始，我们首先扩展G的定义。接下来，我们注意到自a != []年以来(a + b)[0] == a[0].类似地，我们有这个(a + b)[1..] == a[1..] + b，但由于这是另一个序列外延性事实，所以必须明确断言。最后，我们可以使用归纳假设(由Dafny自动调用)来证明G(a[1..] + b) == G(a[1..]) + G(b)。