如何证明将值插入到使用排序数组构建的优先级队列的 dafny 方法？

Question

我在尝试证明和找到下面这个 PQueue 实现的插入方法的前置条件和循环不变量时遇到很多红色问题，有人可以帮忙吗？ ` PQueue 类 {

var size: int
var length: int
var data: array<int>

constructor(capacity: int)
    requires capacity > 0
{
    size := capacity;
    length := 0;
    data := new int[capacity];
}

method insert (pq: PQueue, value: int)

    requires forall i,j :: 0 <= i < j < pq.data.Length ==> pq.data[i] <= pq.data[j]
    requires pq.size > 0 
    requires 0 <= pq.length < pq.size
{
    if (pq.length == pq.size){
        return;
    }

    var i := pq.length-1;
    while i >= 0 && value < pq.data[i]
        invariant 0 <= i <= pq.length - 1
        invariant forall k :: i < k < pq.length ==> pq.data[k] >= value
    {
        pq.data[i+1] := pq.data[i];
        i := i - 1;
    }
    pq.data[i+1] := value;
    pq.length := pq.length + 1;
}`

Answer 1

这是一个稍微更惯用的版本。您需要向 while 循环添加更多不变量，以反映 pqueue 在更新数据之前和之后有效的事实。使用数组需要了解 old() 运算符，并包括值随时间变化的方式的不变量。

    class PQueue {
        var size: int
        var length: int
        var data: array<int>

        constructor(capacity: int)
            requires capacity > 0
            ensures size == capacity
            ensures data.Length == size
            ensures length == 0
            ensures this.Valid()
        {
            size := capacity;
            length := 0;
            data := new int[capacity];
        }

        predicate Valid() 
            reads this, data 
        {
            0 <= size &&
            size == data.Length &&
            0 <= length <= data.Length &&
            forall i,j :: 0 <= i < j < length ==> data[i] <= data[j]
        }
    }

    method insert (pq: PQueue, value: int)
        modifies pq, pq.data
        requires pq.Valid()
        ensures pq.Valid()
        ensures pq.length < pq.size ==> multiset(old(pq.data[..])) + multiset{value} == multiset(pq.data[..])
        ensures pq.length == pq.size ==> multiset(old(pq.data[..])) == multiset(pq.data[..])
    {
        if (pq.length == pq.size) {
            return;
        }

        var i := pq.length-1;
        assert 0<= i < pq.data.Length;
        while 0 <=i < pq.length && value < pq.data[i]
            invariant 0 <= i <= pq.length - 1
            invariant forall k :: i < k < pq.length ==> pq.data[k] >= value
        {
            pq.data[i+1] := pq.data[i];
            i := i - 1;
        }
        pq.data[i+1] := value;
        pq.length := pq.length + 1;
    }