Dafny "call may violate context's modifies clause" error using method invocation inside while loop where "fresh" invariant isn't an option

Question

Below is a simplified (and so useless) version of a Queue class built using linked lists. There is an Add method that adds another (fresh) linked list node to the end of the queue. If I write another method taking a q: Queue as an argument, and run q.Add repeatedly in a while loop, I get a "call may violate context's modifies clause" error that I can't solve using a fresh invariant, because q may already have nodes allocated. Is there a way handling this situation?

class LL {  /* linked list nodes */
  var elem: int;
  var next: LL?;  /* may be null */

  constructor (x: int)
    ensures elem == x && next == null
  {
    elem, next := x, null;
  }
}

class Queue {  // simplified version of queues of integers
  var hd: LL;  // implemented using linked list
  var tl: LL;

  ghost var nodes: seq;  // nodes of linked list

  predicate invar()  // class invariant (ignores elem's)
    reads this, nodes
  {
      nodes != [] && nodes[0] == hd && nodes[|nodes| - 1] == tl &&
      nodes[|nodes| - 1].next == null &&
      (forall i: nat {:trigger nodes[i].next} ::
         i < |nodes| - 1 ==> nodes[i].next == nodes[i + 1])
  }

  constructor ()  // we start with one node
    ensures invar() && |nodes| == 1 && fresh(nodes)
  {
    var l: LL := new LL(0);
    hd, tl := l, l;
    nodes := [l];
  }

  method Add(d: int)  // add another node
    requires invar()
    ensures invar()
    ensures
      nodes != [] && nodes[.. |nodes| - 1] == old(nodes) &&
      fresh(nodes[|nodes| - 1])
    modifies this, nodes
  {
    var l: LL := new LL(d);
    tl.next := l;
    tl := l;
    nodes := nodes + [l];
  }
}

method Foo(q: Queue)
  // if we assume this:
  //   requires q.nodes == []
  // but we want that q may already have some nodes, to which we will add
  requires q.invar()
  modifies q, q.nodes
{
  var i: nat := 0;
  while (i < 10)
    invariant i <= 10
    invariant q.invar()
    // then adding this fresh invariant works:
    //   invariant fresh(q.nodes)
    decreases 10 - i
  {
    q.Add(i);  // error: "call may violate context's modifies clause"
    i := i + 1;
  }
}

user_438267 · Answer

I have two solutions for you. In the first solution, I tried to make minimal changes to the way you set up your data structures, but at the cost that the solution is somewhat hacky/black-magic-y. In the second solution, I show that you can make the proof much cleaner if you are willing to track an additional ghost variable in the queue data structure. The second solution is also in line with idiomatic Dafny style for building these kinds of heap data structures.

First version of first solution: (not quite right, see below)

method Foo(q: Queue)
  requires q.invar()
  modifies q, q.nodes
{
  var i: nat := 0;
  while (i < 10)
    invariant i <= 10
    invariant q.invar()
    invariant forall x :: x in q.nodes ==> x in old(q.nodes) || fresh(x)
    modifies q, q.nodes
    decreases 10 - i
  {
    q.Add(i);
    i := i + 1;
  }
}

We know that q.Add is allowed to modify any node in the current value of q.nodes. To convince Dafny this is safe, we need to maintain the invariant that every element in q.nodes is either in the value of q.nodes from the beginning of Foo, or is fresh since the beginning of Foo.

Unfortunately, just this invariant doesn't quite cut it -- Dafny still reports an error on the call to q.Add. I actually had to drop down to the Boogie level to debug this problem, and it appeared to me to be a case of an overly restrictive trigger on the new loop invariant, which prevented Dafny from having access to the invariant when trying to prove the call to q.Add would not violate the modifies clause.

So I replaced the trigger with the following very aggressive one:

invariant forall x {:trigger allocated(x)} :: x in q.nodes ==> x in old(q.nodes) || fresh(x)

This causes the quantifier to be available for any allocated reference. This causes the program to verify.

Second solution:

The underlying issue here has to do with the encoding of sequences versus sets. When you say that a method can modify a sequence of references, that is slightly harder for the underlying solver to reason about than if you say it modifies a set of references. So I recommend converting your code to tracking sets of references. Here is one way:

class Queue {
  var hd: LL;
  var tl: LL;

  ghost var nodes: seq;
  ghost var footprint: set

Dafny "call may violate context's modifies clause" error using method invocation inside while loop where "fresh" invariant isn't an option

1 Answers