如何证明while循环终止于Dafny

Question

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

关键是引入一个我调用的函数"总电位"；计算循环处理列表所需的迭代次数。它的定义是"；对于列表中的每1，将1加到总电势，对于列表中每非1，将4加到总电势"；。然后，我们将使decreases子句成为总势。这样，当1被移除时，电势下降1，而当非1被移除并被三个1取代时，电势也下降1。

还有一些额外的工作可以让Dafny相信，在每次循环迭代中，总势能实际上都会降低。您将需要一些关于总势能如何与切片和附加序列相关的引理。