Dafny实现优先队列时删除指定索引元素出现越界错误如何解决

问题根源 #

你遇到的循环内赋值索引越界报错，核心原因是循环不变量没有充分刻画两个索引变量的约束关系，Dafny无法自动推导出赋值时indexOfCopy的取值合法。

具体问题点 #

• 现有循环不变量仅约束了indexOfCopy的上限小于capacity，但没有说明indexOfCopy和currentIndex的关系：每次循环最多仅会让indexOfCopy加1，因此indexOfCopy <= currentIndex恒成立，而你已经通过前置条件保证了currentIndex < nrOfElements <= capacity，补充这个约束后Dafny就能推导出indexOfCopy永远不会超过数组长度。
• 额外的小问题：你定义的isEmpty方法逻辑写反了，判断队列空应该返回nrOfElements == 0，你当前的实现会返回相反的结果。

修复后的代码 #

trait PQSpec {
    var nrOfElements: int;
    var capacity: int;
    var contents: array<int>;
    var priorities: array<int>;
    predicate Valid()
    reads this
    {
        0 <= nrOfElements <= capacity && 
        capacity == contents.Length &&
        capacity == priorities.Length 
    }

    method isEmpty() returns (b: bool)
    requires capacity > 0
    {
        return nrOfElements == 0; // 修正逻辑错误
    }
}

class PQImpl extends PQSpec{
    constructor (aCapacity: int)
    requires aCapacity > 0
    ensures Valid(){
        contents :=  new int[aCapacity](_ => 1);
        priorities := new int[aCapacity](_ => -1);
        nrOfElements:= 0;
        capacity := aCapacity;
    }
   method eliminateElementAtIndexFromArray(indexOfElementToBeEliminated: int)
    modifies this
    requires Valid()
    requires indexOfElementToBeEliminated < nrOfElements
    requires indexOfElementToBeEliminated < capacity
    requires nrOfElements <= capacity
    requires nrOfElements > 0
    ensures Valid()
    {   
        var copyOfContents := new int[capacity](_ => 0);
        var copyOfPriorities := new int[capacity](_ => -1);
        var currentIndex := 0;
        var indexOfCopy := 0;

        while(currentIndex < nrOfElements )
        decreases nrOfElements - currentIndex
        invariant currentIndex + 1 <= capacity
        invariant indexOfCopy + 1 <= capacity
        invariant indexOfElementToBeEliminated < nrOfElements
        invariant indexOfCopy <= currentIndex // 新增核心不变量
        {   
            if(indexOfElementToBeEliminated != currentIndex){
                copyOfContents[indexOfCopy] := contents[currentIndex];
                copyOfPriorities[indexOfCopy] := priorities[currentIndex];
                indexOfCopy:=indexOfCopy+1;
            }
            currentIndex:=currentIndex+1;
        }

        contents := copyOfContents;
        priorities := copyOfPriorities;
        nrOfElements := nrOfElements - 1;
    }
}

额外优化建议 #

你当前的删除实现是拷贝整个数组，时间复杂度为O(n)，如果是基于堆实现的优先队列，可以直接把待删除位置的元素和最后一个元素交换，再调整堆结构，时间复杂度可以降到O(logn)，可以根据场景调整实现逻辑。

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