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

问题描述

我是 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 子句。

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

解决方法

没错！这很有挑战性。

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

在 Dafny 中有一个常见的习惯用法是禁止此类事情，使用 repr 鬼域来绑定节点可能传递引用的堆中的引用集。然后，我们定义一个 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 节。 （注意，这篇论文现在已经很老了，所以一些小东西已经过时了。但关键思想还在。）