寻找一个简单循环的不变量

Question

当我试图向 Dafny 证明我的程序是正确的时，我从来没有像现在这样感到如此严重，所以我需要你的帮助：给定的程序如下所示：

method doingMath(N: int, M: int) returns (s: int)
requires N <= M //given precondition
ensures 2*s == M*(M+1)-N*(N+1) //given postcondition
{
    var a: int := N;
    var r: int := 0;

    while a < M 
    invariant FIND ME!
    {
        a := a+1;
        r := r+a;
    }
    return r;
}

作为第一步，我想弄清楚循环的作用，所以我做了一个表格：

这样，我为r 制定了一个循环不变量：

invariant r == (a-N)*N + (a-N)*((a-N)+1)/2

在 (0==0) 之前和循环的每次迭代之后（遵循公式）都成立。显然它不满足终止标准

当循环终止时，循环不变量以及循环终止的原因为我们提供了一个有用的属性。

由于循环保护很简单，我认为完整的不变量应该是

invariant a<=M && r == (a-N)*N + (a-N)*((a-N)+1)/2

因此我的不变量满足初始化、维护和终止。然而，Dafny 抱怨说

错误：循环可能不会维护此循环不变量。

如何让达芙妮开心？

Answer 1

我设法避开了任何非线性算术问题。以下是我对这个问题的看法：

您试图建立一个后置条件，为了清楚起见，我将写为P(s, N, M)，即s、N 和M 的某个函数。提出执行此操作的循环的一种技术是“用变量替换常量”。这意味着您选择所需后置条件的常量之一（在这里，您可以选择N 或M，因为s 不是常量）并将其替换为将要更改的变量在每个循环迭代中。让我们选择M 作为常量并引入（正如您在程序中所做的那样）a 作为变量。由于我们选择了M 作为常量，我们希望a 的最终值是M，所以我们将从a 开始N。然后我们有：

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures P(s, N, M)
{
  var a := N;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)  // postcondition, but with variable a instead of constant M
}

如果你在这个程序中输入（但将P(s, N, a)扩展为实际条件），那么你会发现Dafny证明了后置条件。换句话说，验证器给你的信息是如果你可以建立和保持这个循环不变量，那么程序就会正确地建立后置条件。

您自己也可以看到这一点。循环保护的否定给你M <= a，结合循环不变量a <= M给你a == M。当您结合a == M 和循环不变量P(s, N, a) 时，您将得到后置条件P(s, N, M)。

太好了。但是验证者抱怨说循环不变量在条目上不成立。这是因为我们没有为s 提供任何初始值。由于a 具有初始值N，我们需要为s 找到一个满足P(s, N, N) 的值。该值为0，因此我们将程序更新为

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures P(s, N, M)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)
}

接下来，让我们编写循环体。 （注意我是如何开始使用循环不变量的，而不是从循环体开始然后试图找出一个不变量。对于这类程序，我发现这是最简单的方法。）我们已经决定我们想让a从初始值N变化到最终值M，所以我们添加赋值a := a + 1;：

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant P(s, N, a)
  {
    a := a + 1;
  }
}

这解决了终止问题。我们需要做的最后一件事是在循环内更新s，以便保持不变量。这很容易以目标导向的方式向后完成。方法如下：在循环体的末尾，我们要确保 P(s, N, a) 成立。这意味着我们希望条件P(s, N, a + 1) 在分配给a 之前保持。您可以通过将 desired 条件中的 a 替换为（赋值的右侧）a + 1 来获得此条件（同样，请记住我们正在向后工作）。

好的，所以在分配给a 之前，我们想要P(s, N, a + 1)，而我们在循环体内得到的是不变量P(s, N, a)。现在，是我将P(...) 扩展到您的实际情况的时候了。好的，我们有

2*s == a*(a+1) - N*(N+1)                (*)

我们想要

2*s == (a+1)*(a+2) - N*(N+1)            (**)

让我们将(**) 中的(a+1)*(a+2) 重写为2*(a+1) + a*(a+1)。所以，(**) 等价地可以写成

2*s == 2*(a+1) + a*(a+1) - N*(N+1)      (***)

如果您比较 (***)（这是我们想要的）和 (*)（这是我们已经得到的），那么您会注意到 (***) 的右侧比 2*(a+1) 多(*) 的右侧。所以，我们必须安排左手边增加同样的数量。

如果你将s 增加a+1，那么左边的2*s 增加2*(a+1)，这就是我们想要的。所以，我们的最终程序是

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant 2*s == a*(a+1) - N*(N+1)
  {
    s := s + a + 1;
    a := a + 1;
  }
}

如果需要，您可以将分配的顺序交换为 s 和 a。这会给你

method doingMath(N: int, M: int) returns (s: int)
  requires N <= M
  ensures 2*s == M*(M+1) - N*(N+1)
{
  var a := N;
  s := 0;

  while a < M
    invariant N <= a <= M
    invariant 2*s == a*(a+1) - N*(N+1)
  {
    a := a + 1;
    s := s + a;
  }
}

综上所述，我们从循环不变量构建了循环体，我们通过在后置条件中“用变量替换常量”来设计这个循环不变量。

鲁斯坦

Answer 2

您正在与非线性算术的诅咒发生冲突。每当您依赖乘法的重要属性时，Dafny 都会在您的程序中遇到困难。

这是修复特定证明的一种方法。对不起，它是如此混乱。我确信它可以被清理，但我只是拼凑了一些东西来向你展示这个想法。

function {:opaque} mul(a: int, b: int): int
{
  a * b
}

lemma MulZero1(a: int)
  ensures mul(0, a) == 0
{
  reveal mul();
}

lemma MulNeg1(a: int, b: int)
  ensures mul(-a, b) == -mul(a, b)
{
  reveal mul();
}

lemma MulNeg2(a: int, b: int)
  ensures mul(a, -b) == -mul(a, b)
{
  reveal mul();
}

lemma MulInd(a: nat, b: int)
  ensures mul(a, b) == if a == 0 then 0 else mul(a-1, b) + b
{
  reveal mul();
}

lemma MulEven(a: int, b: int)
  requires b % 2 == 0
  decreases if a < 0 then -a + 1 else a
  ensures mul(a, b) % 2 == 0
{
  if a < 0 {
    MulNeg1(a, b);
    MulEven(-a, b);
  } else if a == 0 {
    MulZero1(b);
  } else {
    calc {
      mul(a, b) % 2;
      { MulInd(a, b); }
      (mul(a-1, b) + b) % 2;
      mul(a-1, b) % 2;
      { MulEven(a-1, b); }
      0;
    }
  }
}

lemma MulComm(a: int, b: int)
  ensures mul(a, b) == mul(b, a)
{
  reveal mul();
}

lemma MulAdjEven(a: int)
  ensures mul(a, a + 1) % 2 == 0
{
  var m := a % 2;

  if m == 0 {
    MulComm(a, a+1);
    MulEven(a+1, a);
  } else {
    assert m == 1;
    assert (a + 1) % 2 == 0;
    MulEven(a, a+1);
  }
}

method doingMath(N: int, M: int) returns (s: int)
requires N <= M //given precondition
ensures 2*s == mul(M,M+1) - mul(N,N+1) //given postcondition
{
    var a: int := N;
    var r: int := 0;

    assert mul(a-N, N) + mul(a-N, (a-N)+1)/2 == 0 by {
      reveal mul();
    }

    while a < M 
      invariant a <= M
      invariant r == mul(a-N, N) + mul(a-N, (a-N)+1)/2
    {
        a := a+1;
        r := r+a;
        assert r == mul(a-N, N) + mul(a-N, (a-N)+1)/2 by {
          reveal mul();
        }
    }

    calc {
      2*r;
      2* (mul(M-N, N) + mul(M-N, (M-N)+1)/2);
      { MulAdjEven(M-N); }
      2*mul(M-N, N) + mul(M-N, (M-N)+1);
      { reveal mul(); }
      mul(M,M+1) - mul(N,N+1);
    }
    return r;
}

对于 Dafny 来说，乘法很难，所以我们手动将它包装在一个不透明的函数中。这让我们可以细粒度地控制何时允许 Dafny “知道”该函数实际上是乘法。

然后我们可以通过调用mul 来替换您方法中出现的所有乘法。这让 Dafny 很快就失败了。 （与超时相比，这是一个很大的改进！）然后我们可以有选择地在我们需要的地方显示mul 的定义，或者我们可以证明关于mul 的引理。

最难的引理是MulEven。尝试用reveal mul(); 替换它的body/proof，你会看到Dafny 超时。相反，我必须通过归纳来证明它。这个证明本身需要关于乘法的其他几个引理。幸运的是，它们都很容易。

---

您可能还想查看作为 IronFleet 项目的一部分开发的数学库 here。 （首先阅读名称中包含“非线性”一词的文件；这些是最接近公理的最低级证明。）他们使用类似的方法来构建大量关于乘法（以及除法和模数）的事实)，这样这些函数就可以在代码库的其他任何地方保持不透明，从而提高 Dafny 的性能。