Dafny实现最大堆时如何编写堆对象修改相关证明引理

开发者阿泽

2026-8-29

Dafny实现迭代版Max-Heapify的堆性质验证问题

问题背景

参考《算法导论》（CLRS 第3版）6.1节（第153页）及维基百科二叉堆词条中的Max-Heapify函数描述，使用Dafny实现最大堆（MaxHeap），将原递归实现改为while循环版本以适配Dafny的验证逻辑。
核心验证目标：调用heapify方法后证明数组满足堆性质，计划通过heapify的requires子句断言：堆中未被修改、更新前已满足堆性质的节点三元组，更新操作后仍然保持堆性质。

遇到的问题

实际验证时发现，只要对数组做修改，验证器就会丢失之前requires子句与循环不变量（invariant）的约束，即使已经证明更新前后对应位置的值完全一致，相关断言仍然无法通过。目前已经将数组元素交换逻辑抽离为独立的swap方法。
尝试编写引理（lemma）证明上述事实时遇到限制：认为Dafny中引理不允许修改堆、使用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]

解决方案

核心问题根源

Dafny验证器不会自动跨数组修改推导谓词成立性，核心原因是MaxHeapChildren是依赖堆对象和数组状态的谓词，仅证明位置值不变，但没有把「值不变+谓词仅依赖对应位置和子节点位置的值」这个逻辑显式传递给验证器。另外引理不能修改状态、不能用old()是认知偏差：引理可以接收数组快照作为参数，等价实现old()的效果，不需要修改堆。

修复步骤

补全swap方法的后置条件证明
现有swap实现中var z:int :| assume ...是错误写法，:|加assume是直接假设存在符合条件的z，没有做实际证明，导致swap的后置条件本身就不成立。删除assume，对任意z做全称量化证明：

// 替换swap方法末尾原有逻辑
forall z {
  if i < z <= heap.data.Length && z != largest {
    assert heap.data[z-1] == old(heap.data[z-1]);
    if left(z) <= heap.data.Length {
      assert left(z) != i;
      assert left(z) != largest;
    }
    if right(z) <= heap.data.Length {
      assert right(z) != i;
      assert right(z) != largest;
    }
    assert heap.MaxHeapChildren(z);
  }
}

修正循环不变量的范围与路径错误
现有不变量forall x :: i <= x <= this.data.Length && x != i' ==> MaxHeapChildren(x)在swap后不成立：swap后i'移动到largest位置，原来的i'位置（oldi）已经满足MaxHeapChildren，但没有被纳入不变量的成立范围；另外原不变量错误限制i'只能是i的直接左右子节点，不符合迭代下沉的实际路径。调整为：
```
invariant i' >= i && (i' == i || oldi == parent(i'))
invariant forall x :: i <= x <= this.data.Length && x != i' && x != oldi ==> MaxHeapChildren(x)
invariant count > 0 ==> MaxHeapChildren(oldi)
```

编写无状态辅助引理
不需要在引理里用old()或者修改堆，直接写接收新旧两个数组的引理，证明如果两个数组在节点z及其子节点位置的值完全相等，那么z在两个数组上的MaxHeapChildren性质等价：

lemma HeapPropertyPreserved(arr_old: array<int>, arr_new: array<int>, z: int)
  requires arr_old.Length == arr_new.Length
  requires 1 <= z <= arr_old.Length
  requires arr_old[z-1] == arr_new[z-1]
  requires left(z) <= arr_old.Length ==> arr_old[left(z)-1] == arr_new[left(z)-1]
  requires right(z) <= arr_old.Length ==> arr_old[right(z)-1] == arr_new[right(z)-1]
  ensures ((left(z) > arr_old.Length || arr_old[z-1] >= arr_old[left(z)-1]) && (right(z) > arr_old.Length || arr_old[z-1] >= arr_old[right(z)-1])) <==>
          ((left(z) > arr_new.Length || arr_new[z-1] >= arr_new[left(z)-1]) && (right(z) > arr_new.Length || arr_new[z-1] >= arr_new[right(z)-1]))
{}

在swap调用后，对所有未修改位置的x调用这个引理，传入old(this.data)和当前this.data，验证器就能自动推导性质保留。

清理冗余逻辑
删除heapify循环里的assume相关语句，去掉重复冗余的断言，保持不变量和后置条件的逻辑闭环即可通过验证。

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

Dafny实现最大堆时如何编写堆对象修改相关证明引理

问题背景 #

遇到的问题 #

现有实现代码 #

测试用例执行流程注释 #

解决方案 #

核心问题根源 #

修复步骤 #