How can I tell Dafny that a method always returns a `new` object?

In this example, I have a method that returns a new array:

method Zeroes(len: nat) returns (h: array<nat>)
  ensures h.Length == len && all_zeroes(h)
{
  h := new nat[len];
  ...
}

and another method that tries to use it:

method Histogram(a: array<nat>, limit: nat) returns (h: array<nat>)
  requires greater_than_all(limit, a)
  ensures h.Length == limit && histogram_of(h, a)
{
  h := Zeroes(limit);
  assert histogram_of_prefix(h, a, 0);

  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant histogram_of_prefix(h, a, i)
  {
    var n := a[i];
    h[n] := h[n] + 1;
    i := i + 1;
  }
}

Dafny complains because it can't prove that Zeroes(limit) won't return a. (If it ever did, my code would be completely broken, Dafny rightly points out.)

It appears that by factoring out Zeroes into a function, I've taken away some information. If I move the body of Zeroes back into Histogram, then Dafny sees h := new nat[limit]; it knows that's not the same array as a, and verification succeeds.

How can I change the signature of Zeroes to tell Dafny that it always returns a new array?

Solution

You can use fresh for that. As in

ensures fresh(h)