对 dafny 中的数字列表求和

Question

我正在使用 dafny 来证明对数字列表求和的不变量：

function sum (s: seq<int>, i: int) : int {
  if |s| == 0 || i == 0 then 0 
  else s[0] + sum(s[1..], i - 1)  
}

/* 
 code: 
 cnt = 0;  
 while i < |input|
   cnt += input[i]; 
   i += 1
*/

method test (input : seq<int>, cnt : int, i : int) 
{
  // invariant: cnt = sum(input, i) && i <= |input| && i >= 0
  // prove that loop invariant is preserved:

  if cnt == sum(input, i) && i <= |input| && i >= 0 && i < |input| 
  { assert (cnt + input[i]) == sum(input, i + 1) && i+1 <= |input| && i+1 >= 0; }
}

dafny 无法验证这一点。我是否缺少 sum 的后置条件？

Answer 1

Dafny 可以证明，但证明需要一些归纳。因此，你必须以这样一种方式来写你的断言，即激发 Dafny 尝试归纳。最简单的方法是写一个引理。通常，简单地写一个断言不会导致 Dafny 尝试归纳证明。

function sum (s: seq<int>, i: int) : int {
  if |s| == 0 || i == 0 then 0 
  else s[0] + sum(s[1..], i - 1)  
}

lemma sumLemma(s: seq<int>, i: int)
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)
{

}

/* 
 code: 
 cnt = 0;  
 while i < |input|
   cnt += input[i]; 
   i += 1
*/

method test (input : seq<int>, cnt : int, i : int) 
{
  // invariant: cnt = sum(input, i) && i <= |input| && i >= 0
  // prove that loop invariant is preserved:

  if cnt == sum(input, i) && i >= 0 && i < |input| 
  { 
      assert i+1 <= |input|;
      assert i+1 > 0;
      sumLemma(input,i);
      assert (cnt + input[i]) == sum(input, i + 1);
  }
}

发生的事情是，当你写引理时，Dafny 猜测归纳步骤可能是什么。如果您关闭 Dafny 的归纳启发式算法，那么它将迫使您调用归纳假设：

lemma {:induction false} sumLemma(s: seq<int>, i: int)
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)
{
  if |s| == 0 || i == 0
  { } else {
    sumLemma(s[1..], i-1);
  }
}

我们在这里所做的是对序列的（归纳）定义或正整数的有根据的（自然）排序进行归纳论证。你通常可以认为归纳证明是基于一些有根据的排序——这里我们可以选择序列的尾部小于序列的排序，除了没有尾部的空序列；或正整数的自然排序。归纳证明技术表明您可以通过以下方式为排序的所有元素证明一些属性：

证明所有最小元素的属性
在假设属性对前任元素成立（我们称此假设为归纳假设）的前提下，为任意其他元素证明属性

所以在我们的例子中，证明有两种情况：

基本情况，序列为空或 i==0 - 其中我们也处于递归函数 sum 的基本情况。 Dafny 直接通过 sum.
归纳案例 - 这里我们调用归纳假设。 sumLemma 适用于序列的尾部和 i-1。 Dafny可以从归纳假设和sum的定义来证明这个案例（你可以认为这是Dafny将sum的定义展开一次）。

为了可靠性，Dafny 还必须证明归纳本身是有根据的。这对应于证明引理 sumLemma 终止。 Dafny 总是证明函数和过程的完全正确性（终止）（除非你告诉它不要，或者在某些特殊情况下）。大多数时候 Dafny 会猜测正确的终止措施，但如果您遇到无法猜测终止措施的情况，您可以提供减少条款。

lemma {:induction false} sumLemma(s: seq<int>, i: int)
   decreases s
   requires i >= 0 && i < |s|
   ensures (sum(s, i) + s[i]) == sum(s, i + 1)

归纳引理和归纳定义的函数在结构上非常相似的原因是我们需要归纳的基本情况与归纳证明的基本情况相对应，以避免必须将 sum 的定义展开 unknown/arbitrary 次（即，如果归纳的基本情况在排序上比 sum 的基本情况高一些步骤）。

您可能会发现，对于一些更困难的引理，Dafny 将无法猜出正确的归纳步骤，而您无论如何都要自己进行归纳调用。

对 dafny 中的数字列表求和

summing a list of numbers in dafny

dafny