如何使对堆对象的更改做出引理？

Question

我正在尝试根据Intro的代码使用DAFNY实现Maxheap。到算法，CLRS第三版，第6.1节，第153页或Max-Heapify函数在这里。我从使用递归转换为一段循环，因为在达夫尼（Dafny）似乎更容易处理。

调用堆功能后，试图证明数组上的堆属性。特别是我希望能够使用heapify上的“要求语句”来断言，在更新之前，在更新之前满足堆属性的堆的三元组不变，在更新后满足了堆属性。

但是，在对数组进行了任何更改之后，似乎忘记了有关要求/不变的语句的所有内容。即使我证明该值在更新之前和之后相同，它仍然不再通过断言。我将更新提取到交换方法中。

我希望我能写一个引理事实，但看来引理不允许修改堆或使用旧（）或调用方法。有没有办法为此编写引理？

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

是的，我认为您要寻找的是a 代码>
基本上，您可以在其规范中使用old（），在呼叫站点中，您可以通过在old（）的呼叫中指定要考虑哪个堆。 @a，如果标签A：在该方法的调用之前存在。