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

编程问答 2022-06-10

问题描述

我是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|

无法使用，如else语句的if部分，seq的大小可能会急剧增加。

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

如何将其转换为达夫尼会同意的代码？

解决方法

这有点棘手，但这是一种实现方法。抱歉，我的解决方案太冗长了。可能有一些方法可以针对行数进行优化，但我希望我编写它的方式至少相当容易理解。

关键是要引入一个函数，该函数计算循环处理列表所需的迭代次数。我将此函数称为TotalPotential。它的定义是“对于列表中的每1，将TotalPotential加1，对于列表中的每非1，将4添加到TotalPotential。然后，将decreases子句设为TotalPotential。这样，当移除1时，电位下降1；当移除非1并被3代替时，电位也下降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报告说，它不能证明减少子句实际上减少了。但是，我们知道！我们只需要说服达夫尼。

    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] + se[..i] + se[i + 1..];
        }
        assert TotalPotential(se) < old_decreases;  // ERROR: assertion violation
    }

请特别注意该错误消息发生了什么。感动了！我们不再收到有关reduces表达式的错误，但是我们确实得到了一个断言违反错误。这是进步，因为这意味着 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] + 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] + se[..i] + se[i + 1..]) < old_decreases;  // ERROR: assertion violation
            // Replace the seq element with 3 occurrences of 1.
            se := [1,1] + se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        }
        assert TotalPotential(se) < old_decreases;
    }

同样，错误消息也会移动。如果我们搞砸了替换操作（例如，根本没有替换！），则if语句每个分支底部的断言仍将带有错误消息。由于这些断言不再包含错误消息，因此我们知道我们已正确替换并正在取得进展。

现在，我们可以使用if表达式，将两个断言从if then else语句的顶部拉出

        assert TotalPotential(if se[i] == 1 then se[..i] + se[i + 1..]
                              else [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] + se[..i] + se[i + 1..]);
              == { TotalPotentialPlus([1,1] + se[..i],se[i + 1..]); }
              TotalPotential([1,1] + se[..i]) + TotalPotential(se[i + 1..]);
              == { TotalPotentialPlus([1,1],se[..i]); }
              TotalPotential([1,1]) + TotalPotential(se[..i]) + TotalPotential(se[i + 1..]);
              == { assert Map(Potential,[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] + se[..i] + se[i + 1..]) < old_decreases;

此词使用相同的引理，但由于现在将三个序列附加在一起而变得更加复杂。还有一个额外的步骤可以说服Dafny，列表[1,1]的总潜力为3。Dafny报告此分支没有进一步的错误！

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

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

function Map<A,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,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,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,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],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] + se[..i] + se[i + 1..]) < old_decreases;
            // Replace the seq element with 3 occurrences of 1.
            se := [1,1] + se[..i] + se[i + 1..];
            assert TotalPotential(se) < old_decreases;
        }
        assert TotalPotential(se) < old_decreases;
    }
}
dafny