在 Dafny 链表实现中使用空引用终止循环

Question

我是 Dafny 的新手，正在尝试编写一个简单的链表实现，它将存储在链表中的所有整数相加。代码如下：

class Node {
var elem: int;
var next: Node?;

constructor (data: int)
{
    elem := data;
    next := null;
}

method addLinkedList() returns (res: int)
{
    res := 0;
    var current := this;
    while(current != null)
    {
        res := res + current.elem;
        current := current.next;
    }
}

}

我有一个简单的节点类，我将整数相加并将指针移动到下一个节点。对我来说很明显，在真正的链表上，这将终止，因为我们最终会到达一个为空的节点，但是我不知道如何向 Dafny 证明这一点。当我使用数组时，总是有一个明显的 decreses 子句，我可以将其添加到 while 循环中，但我不知道这里减少了什么。我尝试将 length 函数编写为：

function length(node:Node?):int
{
    if(node == null) then 0
    else 1 + length(node.next)
}

但是 Dafny 警告我，它也不能证明它的终止，所以我不能将它用作我的 while 循环中的 decreses 子句。

我已经尝试在其他地方搜索，但没有找到任何可以解决此问题的方法，因此非常感谢您的帮助，谢谢。

Answer 1

对！这很有挑战性。

Dafny 担心你的循环和length 函数的事情是，原则上，你可以在堆中构造一个循环列表。然后这些实际上会永远运行！

在 Dafny 中有一个禁止此类事情的常见习惯用法，使用 repr ghost 字段来绑定节点可能传递引用的堆中的引用集。然后，我们定义了一个Valid 谓词，粗略地说，它通过约束this !in next.repr 来保证列表是非循环的。然后我们可以使用repr 作为我们的减少子句。

这是一个完整的工作示例，证明您的 addLinkedList 方法计算列表内容的总和。

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

class Node {
  var elem: int;
  var next: Node?;

  ghost var repr: set<object>;
  ghost var contents: seq<int>;

  constructor (data: int)
    ensures Valid() && contents == [data] && repr == {this}
  {
    elem := data;
    next := null;

    repr := {this};
    contents := [data];
    
  }

  predicate Valid()
    reads this, repr
  {
    && this in repr
    && |contents| > 0
    && contents[0] == elem
    && (next != null ==>
        && next in repr
        && next.repr <= repr
        && this !in next.repr
        && next.Valid()
        && next.contents == contents[1..])
    && (next == null ==> |contents| == 1)
  }

  method addLinkedList() returns (res: int)
    requires Valid()
    ensures res == Sum(contents)
  {
    res := 0;
    var current := this;
    while current != null
      invariant current != null ==> current.Valid()
      invariant res + (if current != null then Sum(current.contents) else 0) 
             == Sum(contents)
      decreases if current != null then current.repr else {}
    {
      res := res + current.elem;
      current := current.next;
    }
  }
}

有关详细信息，请参阅Specification and Verification of Object-Oriented Software 的第 0 节和第 1 节。 （请注意，这篇论文现在已经很老了，所以有些小东西已经过时了。但关键思想在那里。）