While loop termination with null references in Dafny linked list implementation

Question

I am new to Dafny and am trying to write a simple linked list implementation that adds all the integers stored in a linked list. Here is the code:

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

}

I have a simple node class and I am adding the integers up and moving the pointer to the next node. To me it is obvious that on a real linked list this will terminate as we will eventually reach a node which is null, however I do not know how to prove this to Dafny. When I worked with arrays there was always an obvious decreases clause I could add to a while loop, but I am lost as to what decreases here. I have tried writing a length function as:

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

However Dafny warns me that it cannot prove the termination of that either so I cannot use it as a decreases clause on my while loop.

I have tried searching elsewhere but not found anything to remedy this, so any help will be very appreciated, thank you.

Answer 1

Right! This is challenging.

The thing that Dafny is worried about with both your loop and your length function is that, in principle, you could construct a circular list in the heap. Then these would actually run forever!

There is a common idiom to forbidding such things in Dafny, using a repr ghost field to bound the set of references in the heap that the node might transitively refer to. We then define a Valid predicate, which, among other things, guarantees that the list is acyclic by constraining this !in next.repr, roughly speaking. Then we can use repr as our decreases clause.

Here is a complete working example proving that your addLinkedList method computes the sum of the contents of the list.

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

For more information, see sections 0 and 1 of Specification and Verification of Object-Oriented Software. (Note that this paper is quite old now, so some minor things are out of date. But the key ideas are there.)