如何对堆对象的更改进行引理？

Question

我正在尝试根据 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 := data;
        this.repr := {this};
    }
    
    predicate method MaxHeapChildren(i: int)
        reads this, this.data
        requires 1 <= i
    {
        (left(i) > this.data.Length || this.data[i-1] >= this.data[left(i)-1]) && (right(i) > this.data.Length || this.data[i-1] >= this.data[right(i)-1])
    }

    method heapify(i: int) returns (largest: int)
        modifies this.data
        requires 1 <= i <= this.data.Length
        requires forall x :: i < x <= this.data.Length ==> MaxHeapChildren(x)
        // ensures multiset(this.data[..]) == multiset(old(this.data[..]))
        ensures forall x :: i <= x <= this.data.Length  ==> MaxHeapChildren(x)
        decreases this.data.Length - i
    {
        var i' := i;
        ghost var oldi := i;
        largest := i;
        var l := left(i);
        var r := right(i);
        ghost var count := 0;
        ghost var count' := 1;
        while !MaxHeapChildren(i')
            invariant count' == count + 1;
            invariant 1 <= largest <= this.data.Length
            invariant l == left(i')
            invariant r == right(i')
            invariant 1 <= i' <= this.data.Length
            invariant i' == i || i' == left(oldi) || i' == right(oldi)
            invariant largest == i'
            invariant count == 0 ==> oldi == i
            invariant oldi > 0
            invariant count > 0 ==> oldi == parent(i')
            invariant count > 0 ==> MaxHeapChildren(oldi)
            invariant count > 0 ==> forall x :: i <= x < i' ==> old(this.data)[x] == this.data[x]
            invariant count > 0 ==> forall x :: i <= x < i' && left(x+1) < this.data.Length ==> old(this.data)[left(x+1)] == this.data[left(x+1)]
            invariant count > 0 ==> forall x :: i <= x < i' && right(x+1) < this.data.Length ==> old(this.data)[right(x+1)] == this.data[right(x+1)]
            // invariant count > 0 ==> forall x :: i <= x <= i' && left(x+1) ==> MaxHeapChildren(left(x+1))
            invariant forall x :: i <= x <= this.data.Length && x != i' ==> MaxHeapChildren(x)
            decreases this.data.Length-i';
        {
            if l <= this.data.Length && this.data[l-1] > this.data[i'-1] {
                largest := l;
            }

            if r <= this.data.Length && this.data[r-1] > this.data[largest-1] {
                largest := r;
            }
            if largest != i' {
                assert forall x :: i <  x <= this.data.Length && x != i' ==> MaxHeapChildren(x);
                swap(this, i', largest);
                label AfterChange:
                oldi := i';
                assert MaxHeapChildren(oldi);
                i' := largest;
                assert forall x :: largest <  x <= this.data.Length && x != i' ==> MaxHeapChildren(x);
                l := left(i');
                r := right(i');
                
                assert forall x :: i <= x < i' ==> old@AfterChange(this.data[x]) == this.data[x] && left(x+1) < this.data.Length ==> old(this.data)[left(x+1)] == this.data[left(x+1)] && right(x+1) < this.data.Length ==> old(this.data)[right(x+1)] == this.data[right(x+1)];
            }else{
                assert MaxHeapChildren(i');
                assert MaxHeapChildren(oldi);
            }
            count := count + 1;
            count' := count' + 1;
        }
    }
}

method swap(heap: MaxHeap, i: int, largest: int) 
    modifies heap.data
    requires 1 <= i < largest <= heap.data.Length
    requires heap.data[largest-1] > heap.data[i-1]
    requires left(i) <= heap.data.Length ==> heap.data[largest-1] >= heap.data[left(i)-1]
    requires right(i) <= heap.data.Length ==> heap.data[largest-1] >= heap.data[right(i)-1]
    requires forall x :: i <= x <= heap.data.Length && x != i ==> heap.MaxHeapChildren(x)
    ensures heap.data[i-1] == old(heap.data[largest-1])
    ensures heap.data[largest-1] == old(heap.data[i-1])
    ensures heap.MaxHeapChildren(i)
    ensures forall x :: 1 <= x <= heap.data.Length && x != i && x != largest ==> heap.data[x-1] == old(heap.data[x-1]) 
    ensures forall x :: i <= x <= heap.data.Length && x != largest ==> heap.MaxHeapChildren(x)
{
    ghost var oldData := heap.data[..];
    var temp := heap.data[i-1];
    heap.data[i-1] := heap.data[largest-1];
    heap.data[largest-1] := temp;
    var z:int :| assume i < z <= heap.data.Length && z != largest;
    var lz: int := left(z);
    var rz: int := right(z);
    assert heap.data[z-1] == old(heap.data[z-1]);
    assert lz != i && lz != largest && lz <= heap.data.Length ==> heap.data[lz-1] == old(heap.data[lz-1]);
    assert rz != i && rz != largest && rz <= heap.data.Length ==> heap.data[rz-1] == old(heap.data[rz-1]);
    assert heap.MaxHeapChildren(z);

}

/**
        heapify(4)
        length = 17
        i = 4
        left = 8, 7 (0based)
        right = 9, 8 (0based)
        x in 5 .. 17 :: MaxHeapChildren(x) (i+1)..17 

         0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 
        [20,18,16,3,14,12,10, 8, 6, 4, 2, 0, 1,-2, 4, 4,-5]


        i = 8
        left = 16
        right = 17
        x in i' .. i-1 :: MaxHeapChildren (4..15)
         0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 
        [20,18,16,8,14,12,10, 3, 6, 4, 2, 0, 1,-2, 4, 4,-5]


        i = 16
        left = 32
        right = 33
        x in i' .. i-1 :: MaxHeapChildren (4..16) + 17.. MaxHeapChildren
         0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 
        [20,18,16,8,14,12,10, 4, 6, 4, 2, 0, 1,-2, 4, 3,-5]
     */

Answer 1

是的，我认为您正在寻找的内容称为 atwostate lemma 基本上，您可以在他们的规范中使用，并且在调用站点，您可以通过在引理名称后缀 来old()指定要考虑调用哪个堆（如果 在该方法调用之前存在） 。old()@alabel a: