在 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;
    }
}

}

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

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

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

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

Answer 1

对了！这很有挑战性。

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;
    }
  }
}

有关详细信息，请参阅规范和验证的第 0 节和第 1 节面向对象软件。（请注意，这篇论文现在已经很老了，所以一些小的东西已经过时了。但是关键思想在那里。）

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

While loop termination with null references in Dafny linked list implementation

formal-verification

dafny