如何证明 while 循环在 Dafny 中终止？

Question

我是 Dafny 的新手，正在学习它。对于以下 Dafny 代码

method Dummy(s: seq<nat>) returns (ret: nat)
    requires forall k :: 0 <= k < |s| ==> s[k] > 0
{
    ret := 0;
    var se := s;

    while |se| > 0
    {
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
        } else {
            // Replace the seq element with 3 occurences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
        }
    }

    return;
}

我看到的投诉是

decreases |se| - 0Dafny VSCode
cannot prove termination; try supplying a decreases clause for the loopDafny VSCode

我知道要证明终止，一般我应该提供一个decreases条款。在这种情况下，我只是找不到要放在 decreases 子句中的内容。简单地说

decreases |se|

不会起作用，因为在 if 语句的 else 部分中 seq 大小可能会实际增加。

如果这是纸笔证明，我想证明对于任何为1的元素，它都会被删除；对于任何大于 1 的元素，它将被 3 次出现的 1 替换，最终仍将被删除。因此 se 最后将为空，循环终止。

如何将其转换为 Dafny 同意的代码？

Answer 1

这个有点棘手，但这是一种方法。很抱歉我的解决方案如此long-winded。可能有一些方法可以针对行数对其进行优化，但我希望我编写它的方式至少相当简单易懂。

关键是引入一个函数来计算循环处理列表所需的迭代次数。我称这个函数为TotalPotential。它的定义是“对于列表中的每一个 1，将 1 添加到 TotalPotential，对于列表中的每个非 1，将 4 添加到 TotalPotential”。然后，我们将 decreases 子句设为 TotalPotential。这样，当一个 1 被移除时，势能下降 1，当一个非 1 被移除并被三个 1 取代时，势能也下降 1.

为了在 Dafny 中定义 TotalPotential，我将在序列上使用一些通用函数。 Sum 将自然数列相加。 Map 将函数应用于序列的每个元素。

function Sum(s: seq<nat>): nat
{
  if s == []
  then 0
  else s[0] + Sum(s[1..])
}

function Map<A,B>(f: A -> B, s: seq<A>): seq<B> {
  if s == []
  then []
  else [f(s[0])] + Map(f, s[1..])
}

我们可以如下计算列表中单个元素的潜力。

function Potential(x: nat): nat
{
  if x == 1
  then 1
  else 4
}

然后 TotalPotential 是映射 Potential 在列表上的总和。

function TotalPotential(s: seq<nat>): nat
{
  Sum(Map(Potential, s))
}

现在我们将 decreases TotalPotential(se) 添加到 while 循环中。 Dafny 报告说，它无法证明减少条款实际上减少了。但我们知道它确实如此！我们只需要说服 Dafny。

    while |se| > 0
      decreases TotalPotential(se)  // ERROR: decreases expression might not decrease
    {
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
        } else {
            // Replace the seq element with 3 occurrences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
        }
    }

为了调试它，让我们尝试了解 Dafny 被卡住的地方。当 Dafny 证明减少表达式减少时，它会将循环迭代开始时的表达式值与该循环迭代结束时的值进行比较。我们可以引入一个幽灵变量来保存这个表达式的旧值，然后断言在循环的底部，这个值已经减少了。

    while |se| > 0
      decreases TotalPotential(se)
    {
        ghost var old_decreases := TotalPotential(se);
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
        } else {
            // Replace the seq element with 3 occurrences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
        }
        assert TotalPotential(se) < old_decreases;  // ERROR: assertion violation
    }

请仔细注意错误信息发生了什么。它动了！我们不再收到关于 decreases 表达式的错误，但我们确实收到断言违规错误。这是进步，因为这意味着if我们可以证明断言，那么我们就证明了终止。换句话说，我们已经成功地找到了一种方法来访问 Dafny 卡住的内容。

现在我们可以对该断言使用常用的调试技术。因为断言比较两个不同“时间点”的值，所以我喜欢尝试将断言向后移动到 old_decreases 的定义。首先，我们可以将断言的副本移动到 if 语句的每个分支中。

    while |se| > 0
      decreases TotalPotential(se)
    {
        ghost var old_decreases := TotalPotential(se);
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;  // ERROR: assertion violation
        } else {
            // Replace the seq element with 3 occurrences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;  // ERROR: assertion violation
        }
        assert TotalPotential(se) < old_decreases;
    }

再次注意错误消息的移动方式。底部的断言不再失败，但我们必须证明这两个新断言。 Dafny 告诉我们“如果你可以证明这两个新断言，那么底部的断言就会随之而来。

现在让我们通过替换右侧将这些断言向后转换为 se 的赋值。

    while |se| > 0
      decreases TotalPotential(se)
    {
        ghost var old_decreases := TotalPotential(se);
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            assert TotalPotential(se[..i] + se[i + 1..]) < old_decreases;  // ERROR: assertion violation
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        } else {
            assert TotalPotential([1, 1, 1] + se[..i] + se[i + 1..]) < old_decreases;  // ERROR: assertion violation
            // Replace the seq element with 3 occurrences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        }
        assert TotalPotential(se) < old_decreases;
    }

再次，错误消息移动。如果我们搞砸了我们的替换（例如，根本没有替换！），if 语句每个分支底部的断言仍然会有错误消息。由于这些断言不再有错误消息，我们知道我们正确地替换了并且正在取得进展。

现在我们可以使用 if then else 表达式从 if 语句的顶部提取两个断言，就像这样

        assert TotalPotential(if se[i] == 1 then se[..i] + se[i + 1..]
                              else [1, 1, 1] + se[..i] + se[i + 1..])
               < old_decreases;

但是继续向上移动断言并没有真正的优势，因为在我们即将做的证明中，我们只需要再次分支判断 se[i] 是否为 1。所以让我们坚持我们的两个断言，一个在每个分支的顶部。

现在是做一些证明的时候了。我喜欢使用 calc 语句来证明这些不等式（或等式）。这是第一个。

            calc {
              TotalPotential(se[..i] + se[i + 1..]);
              == { TotalPotentialPlus(se[..i], se[i + 1..]); }
              TotalPotential(se[..i]) + TotalPotential(se[i+1..]);
              < TotalPotential(se[..i]) + Potential(se[i]) + TotalPotential(se[i+1..]);
              == { DecomposeTotalPotential(se, i); }
              TotalPotential(se);
            }
            assert TotalPotential(se[..i] + se[i + 1..]) < old_decreases;

这个证明使用了两个引理。首先，附加在一起的两个序列的总潜力等于第一个序列的总潜力加上第二个序列的总潜力。其次，se的总势可以写成索引i之前元素的总势加上索引i处元素的势，再加上所有元素的总势在索引 i 之后。所有引理和证明都出现在这个答案的底部。请注意，此 calc 语句有一行以 < 运算符开头。这意味着这个 calc 语句的结论将是下面断言的不等式。 Dafny 报告此分支上不再有错误！

这是第二个证明。

            calc  {
              TotalPotential([1, 1, 1] + se[..i] + se[i + 1..]);
              == { TotalPotentialPlus([1, 1, 1] + se[..i], se[i + 1..]); }
              TotalPotential([1, 1, 1] + se[..i]) + TotalPotential(se[i + 1..]);
              == { TotalPotentialPlus([1, 1, 1], se[..i]); }
              TotalPotential([1, 1, 1]) + TotalPotential(se[..i]) + TotalPotential(se[i + 1..]);
              == { assert Map(Potential, [1, 1, 1]) == [1, 1, 1]; }
              3 + TotalPotential(se[..i]) + TotalPotential(se[i + 1..]);
              < TotalPotential(se[..i]) + 4 + TotalPotential(se[i + 1..]);
              == TotalPotential(se[..i]) + Potential(se[i]) + TotalPotential(se[i + 1..]); 
              == { DecomposeTotalPotential(se, i); }
              TotalPotential(se);
            }
            assert TotalPotential([1, 1, 1] + se[..i] + se[i + 1..]) < old_decreases;

这个使用相同的引理，但有点复杂，因为现在有三个序列被附加在一起。还有一个额外的步骤让 Dafny 相信列表的总潜力 [1, 1, 1] 是 3。Dafny 报告此分支上没有进一步的错误！

这是完整的程序，带有引理和证明。

function Sum(s: seq<nat>): nat
{
  if s == []
  then 0
  else s[0] + Sum(s[1..])
}

function Map<A,B>(f: A -> B, s: seq<A>): seq<B> {
  if s == []
  then []
  else [f(s[0])] + Map(f, s[1..])
}

function Potential(x: nat): nat
{
  if x == 1
  then 1
  else 4
}

function TotalPotential(s: seq<nat>): nat
{
  Sum(Map(Potential, s))
}

lemma MapPlus<A,B>(f: A -> B, s1: seq<A>, s2: seq<A>)
  ensures Map(f, s1 + s2) == Map(f, s1) + Map(f, s2)
{
  if s1 == [] {
    assert s1 == [];
    calc {
      Map(f, s1 + s2);
      {
        assert s1 + s2 == s2;
      }
      Map(f, s2);
      Map(f, s1) + Map(f, s2);
    }
  } else {
    calc {
      Map(f, s1 + s2);
      {
        assert s1 != [];
        assert (s1 + s2) != [];
        assert (s1 + s2)[0] == s1[0];
        assert (s1 + s2)[1..] == s1[1..] + s2;
      }
      [f(s1[0])] + Map(f, s1[1..] + s2);
      [f(s1[0])] + (Map(f, s1[1..]) + Map(f, s2));
      Map(f, s1) + Map(f, s2);
    }
  }
}

lemma SumPlus(s1: seq<nat>, s2: seq<nat>)
  ensures Sum(s1 + s2) == Sum(s1) + Sum(s2)
{
  if s1 == [] {
    assert s1 == [];
    assert s1 + s2 == s2;
  } else {
    calc {
      Sum(s1 + s2);
      {
        assert s1 != [];
        assert (s1 + s2) != [];
        assert (s1 + s2)[0] == s1[0];
        assert (s1 + s2)[1..] == s1[1..] + s2;
      }
      s1[0] + Sum(s1[1..] + s2);
      Sum(s1) + Sum(s2);
    }
  }
}

lemma TotalPotentialPlus(s1: seq<nat>, s2: seq<nat>)
  ensures TotalPotential(s1 + s2) == TotalPotential(s1) + TotalPotential(s2)
{
  MapPlus(Potential, s1, s2);
  SumPlus(Map(Potential, s1), Map(Potential, s2));
}

lemma DecomposeTotalPotential(s: seq<nat>, i: int)
  requires 0 <= i < |s|
  ensures
    TotalPotential(s)
    == TotalPotential(s[..i]) + Potential(s[i]) + TotalPotential(s[i + 1..])
{
  calc {
    TotalPotential(s);
    {
      assert s == (s[..i] + [s[i]]) + s[i + 1..];
      TotalPotentialPlus(s[..i] + [s[i]], s[i + 1..]);
    }
    TotalPotential( s[..i] + [s[i]]) + TotalPotential(s[i+1..]);
    { TotalPotentialPlus(s[..i], [s[i]]); }
    TotalPotential(s[..i]) + TotalPotential([s[i]]) + TotalPotential(s[i + 1..]);
    { assert TotalPotential([s[i]]) == Sum(Map(Potential, [s[i]])); }
    TotalPotential(s[..i]) + Potential(s[i]) + TotalPotential( s[i + 1..]);
  }
}

method Dummy(s: seq<nat>) returns (ret: nat)
    requires forall k :: 0 <= k < |s| ==> s[k] > 0
{
    ret := 0;
    var se := s;

    while |se| > 0
      decreases TotalPotential(se)
    {
        ghost var old_decreases := TotalPotential(se);
        // Pick a random index of the seq.
        var i :| 0 <= i < |se|;
        if se[i] == 1 {
            calc {
              TotalPotential(se[..i] + se[i + 1..]);
              == { TotalPotentialPlus(se[..i], se[i + 1..]); }
              TotalPotential(se[..i]) + TotalPotential(se[i+1..]);
              < TotalPotential(se[..i]) + Potential(se[i]) + TotalPotential(se[i+1..]);
              == { DecomposeTotalPotential(se, i); }
              TotalPotential(se);
            }
            assert TotalPotential(se[..i] + se[i + 1..]) < old_decreases;
            // Remove the seq element if it is 1.
            se := se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        } else {
            calc  {
              TotalPotential([1, 1, 1] + se[..i] + se[i + 1..]);
              == { TotalPotentialPlus([1, 1, 1] + se[..i], se[i + 1..]); }
              TotalPotential([1, 1, 1] + se[..i]) + TotalPotential(se[i + 1..]);
              == { TotalPotentialPlus([1, 1, 1], se[..i]); }
              TotalPotential([1, 1, 1]) + TotalPotential(se[..i]) + TotalPotential(se[i + 1..]);
              == { assert Map(Potential, [1, 1, 1]) == [1, 1, 1]; }
              3 + TotalPotential(se[..i]) + TotalPotential(se[i + 1..]);
              < TotalPotential(se[..i]) + 4 + TotalPotential(se[i + 1..]);
              == TotalPotential(se[..i]) + Potential(se[i]) + TotalPotential(se[i + 1..]); 
              == { DecomposeTotalPotential(se, i); }
              TotalPotential(se);
            }
            assert TotalPotential([1, 1, 1] + se[..i] + se[i + 1..]) < old_decreases;
            // Replace the seq element with 3 occurrences of 1.
            se := [1, 1, 1] + se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        }
        assert TotalPotential(se) < old_decreases;
    }
}

如何证明 while 循环在 Dafny 中终止？

How do I prove the while loop terminates in Dafny?

dafny