Dafny "call might violate context's modifies clause"

sligocki 0
Viewed 63

I'm new to Dafny. I'm getting the error: call might violate context's modifies clause on the line where Seek() calls Step() in the following code:

class Tape {
  var val : int;

  constructor() {
    this.val := 0;
  }

  method Write(x : int)
    modifies this
  {
    this.val := x;
  }
}

class Simulator {
  var tape : Tape;
  var step_num : nat;

  constructor() {
    this.tape := new Tape();
    this.step_num := 0;
  }

  method Step()
    modifies this, this.tape
    ensures this.step_num > old(this.step_num)
  {
    this.tape.Write(1);
    this.step_num := this.step_num + 1;
  }

  method Seek(target_step_num : int)
    modifies this, this.tape
  {
    while this.step_num < target_step_num {
      this.Step();
    }
  }
}

I don't understand what's going on here because I explicitly annotated Seek() with modifies this, this.tape.

Looking around online I see some talk about "freshness" and I get the impression that this has to do with ensuring that I have permission to access this.tape, but I don't understand how to fix it. Thanks!

dafny
2 Answers

You need invariant that this.tape is not reassigned to something else in methods. Adding ensures this.tape == old(this.tape) post condition in Seek and Step and also adding invariant this.tape == old(this.tape) fixes it.

Divyanshu Ranjan0

FWIW, in addition to Divyanshu's excellent answer, I also discovered that I could fix this issue by defining tape as a const:

class Simulator {
  const tape : Tape;
  var step_num : nat;
  ...

In this case, it appears that const means that the pointer/reference will never be modified (that it will never point to a different Tape object), not that the Tape object itself will be unmodified.

sligocki0
Related