我怎样才能告诉Dafny一个方法总是返回一个“new”对象?

In this example ,我有一个返回新数组的方法:

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

还有另一种尝试使用它的方法:

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抱怨,因为它不能证明这一点 Zeroes(limit) 不会再回来了 a (达夫尼正确地指出,如果真是这样的话,我的代码将被完全破坏。)

看来通过分解 Zeroes 在函数中,我带走了一些信息。如果我移动 零 返回到 Histogram ,然后Dafny看到 h := new nat[limit]; 它知道这和 A. ,验证成功。

如何更改的签名 零 告诉Dafny它总是返回一个新数组?