小编Hat*_*995的帖子

我正在尝试根据 Intro 中的代码使用 Dafny 实现 MaxHeap。参见《算法》，CLRS 第 3 版，第 6.1 节，第 153 页或此处的Max-Heapify 函数。我从使用递归切换到 while 循环，因为这在 Dafny 中似乎更容易处理。

调用 heapify 函数后尝试证明数组的堆属性。特别是，我希望能够使用 heapify 上的 require 语句来断言堆中未更改且在更新之前满足堆属性的三元组在更新后也满足堆属性。

然而，对数组进行任何更改后，它似乎忘记了所有有关 require/invariant 语句的信息。即使我表明更新前后的值相同，它仍然不再通过断言。我将更新提取到交换方法中。

我希望我可以写一个引理来断言这个事实，但似乎引理不允许修改堆或使用 old() 或调用方法。有没有办法为此写一个引理？

function method parent(i: int): int 
{
    i/2
}

function method left(i: int): int
{
    2*i
}

function method right(i: int): int
{
    2*i+1
}


class MaxHeap {
    var data: array<int>
    ghost var repr: set<object>

    constructor(data: array<int>) 
        ensures this.data == data
        ensures this in repr
    {
        this.data := …