在 Dafny 中删除特定索引处的元素失败

Question

我有以下问题：我必须在 Dafny 中实现一个优先级队列。我有如下界面：

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; 
}

我没有在特征中插入抽象方法，因为它们与我的问题无关

nrOfElements - 将保存优先级队列中的元素数量

容量 - 将保存可以存储的最大元素数

contents 将保存值

priorities 将保留优先级

有效 - 应该确保我的优先级队列在 nrOfElements 和容量方面是有效的（或者至少我希望我这样做）

问题出在下面这段代码：

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
        {   
            assert nrOfElements <= capacity
            assert currentIndex <= nrOfElements + 1;
            assert indexOfCopy < capacity;
            if(indexOfElementToBeEliminated != currentIndex){
                copyOfContents[indexOfCopy] := contents[currentIndex];
                copyOfPriorities[indexOfCopy] := priorities[currentIndex];
                indexOfCopy:=indexOfCopy+1;
            }
            
            currentIndex:=currentIndex+1;
                    
        }

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

我尝试做的是从数组中删除在给定索引处找到的元素。这样做的方法是简单地创建一个新数组而不包含该值。但是，每当我在 while 中进行分配时，都会遇到索引越界错误。

任何帮助将不胜感激！

Answer 1

您现有的循环不变量都不是必需的。您需要几个新的不变量：

while currentIndex < nrOfElements
    invariant this.Valid()
    invariant this.capacity == old(this.capacity)
    invariant 0 < this.nrOfElements
    invariant indexOfCopy <= currentIndex
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

请注意，前三个不变量与this 的字段有关。 （为了强调，我在所有字段中都明确包含了this.。）但是这个循环根本不会改变this！它只会更改新分配的数组。默认情况下，Dafny 假定您希望循环修改允许该方法修改的所有内容，因此循环上的默认修改子句包括 this，因为包含方法有一个包含 this 的修改子句。我们可以通过在循环上提供一个显式的修改子句来覆盖默认值，该子句声明只有这些数组被修改。然后你可以删除前三个不变量，如下所示：

while currentIndex < nrOfElements
    modifies copyOfContents, copyOfPriorities
    invariant indexOfCopy <= currentIndex
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

如果您愿意，最后一个版本的另一种等效方法是使用unchanged 表示this 未被循环修改：

while currentIndex < nrOfElements
    invariant indexOfCopy <= currentIndex
    invariant unchanged(this)
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

我更喜欢使用 modifies 子句而不是 unchanged，因为 modifies 子句允许我们向求解器表达语法上的变化，而 unchanged 仅使用附加的不变量表达“事后”语义上的变化。但它们都工作得很好，所以你应该选择你更喜欢的一个。