Modifies clause error on a changed object

问题:

How can I state (in Dafny) an "ensures" guarantee that the object returned by a method will be "new", i.e., will not be the same as an object used anywhere else (yet)?

The following code shows a minimal example:

method newArray(a:array<int>) returns (b:array<int>)
requires a != null
ensures b != null
ensures a != b
ensures b.Length == a.Length+1
{
  b := new int[a.Length+1];
}

class Testing {
  var test : array<int>;

  method doesnotwork()
  requires this.test!=null
  requires this.test.Length > 10;
  modifies this
  {
    this.test := newArray(this.test); //change array a with b
    this.test[3] := 9;  //error modifies clause
  }

  method doeswork()
  requires this.test!=null
  requires this.test.Length > 10;
  modifies this
  {
    this.test := new int[this.test.Length+1];
    this.test[3] := 9;
  }


}

The "doeswork" function compiles (and verifies) correctly, but the other one does not, as the Dafny compiler cannot know that the object returned by the "newArray" function is new, i.e., is not required to be listed as modifiable in the "require" statement of the "doesnotwork" function in order for that function to fulfill the requirement that it only modifies "this". In the "doeswork" function, I simply inserted the definition of the "newArray" function, and then it works.

You can find the example above under https://rise4fun.com/Dafny/hHWwr, where it can also be ran online.

Thanks!

回答1:

You can say ensures fresh(b) on newArray.

fresh means exactly what you described: the object is not the same as any object that was allocated before the call to newArray.