如何修改Dafny中Zeroes方法签名以表明其始终返回全新数组？

我有一个用于返回新数组的方法Zeroes：

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

还有一个调用该方法的Histogram方法：

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提取为独立方法后，似乎丢失了部分关键信息。如果将Zeroes的实现直接移回Histogram中，Dafny能直接识别到h := new nat[limit];是一个与a完全不同的新数组，验证就能顺利通过。

那么问题来了：如何修改Zeroes的方法签名，以告知Dafny它始终返回全新数组？

解决方案 #

要让Dafny确认Zeroes返回的是全新数组，你需要在方法的ensures后置条件中添加数组新鲜性断言——使用Dafny内置的fresh(h)谓词，它专门用来表示h是一个在方法调用前不存在的新对象。

修改后的Zeroes方法签名如下：

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

添加fresh(h)后，Dafny就明确知道该方法返回的数组是全新创建的，不可能和传入Histogram的a是同一个数组，验证也就能够顺利通过了。

你也可以用h !in old(Heap)来进一步明确新数组与所有已有数组不重叠，但fresh(h)是表达“返回全新数组”更简洁的标准写法。

内容的提问来源于stack exchange，提问作者Jason Orendorff