1

我正在使用 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吗？

4

1 回答 1

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

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

  1. 证明所有最小元素的性质
  2. 证明任意其他元素的属性，假设该属性适用于前驱元素（我们将此假设称为归纳假设）

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

  1. 基本情况，序列为空或i==0- 在这种情况下，我们也是递归函数的基本情况sum。Dafny 很容易通过 的定义直接证明这种情况sum。

  2. 归纳案例——这里我们调用归纳假设。这 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问题未知/任意次数（即，如果归纳的基本情况在排序中比 的基本情况高一些步骤sum）。

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

于 2016-05-23T09:44:48.283 回答