Dafny

Question

以下内容基于 Secure Foundations's dafny implementation of a Dynamic Array。

我正在尝试创建一个测试方法，在调用 push_back 时调用 extend_buffer。这需要一个前缀：调用 push_back 足够的次数来填满它，这样下次调用它时，缓冲区就会被扩展。默认大小为 16，前缀将包含调用 push_back 15 次。我发现如果我调用 15 次它会验证，但如果我改为尝试在 for 循环中调用，我会收到错误 call may violate context's modifies clause.

class Vector<T> {

    static const DEFAULT_SIZE := 16
    var buffer : array<T>
    var capacity : int
    var size : int

    predicate Valid()
    reads this, buffer
    {
        capacity >= DEFAULT_SIZE
        && capacity as int == buffer.Length
        && 0 <= size < capacity
    }

    method extend_buffer(value: T)
    requires Valid()
    ensures Valid()
    ensures fresh(buffer)
    ensures size as int < capacity as int - 1
    ensures forall i : int :: 0 <= i < old(size) ==> buffer[i] == old(buffer[i])
    ensures size == old(size)
    ensures capacity == old(capacity) as int * 2
    ensures buffer.Length == old(buffer.Length) * 2
    modifies this`capacity, this`buffer
    {
        var old_buffer := this.buffer;
        var old_size := this.capacity;


        capacity := old_size * 2;
        buffer := newArrayFill(capacity, value);

        var i:= 0;
        while i < old_size
        invariant Valid();
        invariant capacity > old_size;
        invariant i < capacity;
        invariant i < old_size;
        invariant fresh(buffer)
        invariant size < capacity - 1;
        invariant size == old(size)
        invariant capacity == old(capacity) * 2
        invariant forall k : int :: 0 <= k < i ==> buffer[k] == old_buffer[k] == old(buffer[k])
        {
            buffer[i] := old_buffer[i];

            if i == old_size - 1 {
                break;
            }
            i := i + 1;
        }
    }

    method push_back(value:T)
    requires Valid()
    ensures Valid();
    ensures old(size as int) < buffer.Length
    ensures buffer[old(size)] == value
    ensures size == old(size) + 1
    ensures if old(size) + 1 == old(capacity) then fresh(buffer) else buffer == old(buffer)
    ensures forall i : int :: 0 <= i < old(size) ==> buffer[i] == old(buffer[i])
    ensures forall i : int :: size <= i < old(buffer.Length) ==> buffer[i] == old(buffer[i])
    ensures if size == old(capacity) then fresh(buffer) else !fresh(buffer) && buffer == old(buffer)
    modifies this, this.buffer, this`size
    {
        if (size + 1 == capacity)
        {
            extend_buffer(value);
        }
        buffer[size] := value;
        size := size + 1;
    }

    method {:extern "Extern", "newArrayFill"} newArrayFill<T>(n: int, t: T) returns (ar: array<T>)
    ensures ar.Length == n as int
    ensures forall i | 0 <= i < n :: ar[i] == t
    ensures fresh(ar)

    constructor(default_val:T)
    ensures Valid()
    ensures fresh(buffer)
    ensures size == 0
    ensures capacity == DEFAULT_SIZE 
    ensures capacity as int == buffer.Length
    {
        size := 0;
        capacity := DEFAULT_SIZE;
        new;
        buffer := newArrayFill(DEFAULT_SIZE, default_val);
    }
}

method push_back_should_extend()
{
    var arr := new Vector(0);
    label L:
    var oracleValue := 7;

    for i : int := 0 to arr.capacity - 1
    invariant arr.Valid()
    {
        arr.push_back(oracleValue);
    }

}

我假设问题是由于 push_back 声称它修改了 this，我觉得这夸大了它实际修改的内容，但是当我删除 this 时，错误只是移动到对 extend_buffer.

的调用

有趣的是，添加以下两个状态：

twostate predicate sameBuffer(v: Vector)
reads v`buffer
{
    v.buffer == old(v.buffer)
}

然后将 invariant sameBuffer@L(arr) 添加到 push_back_should_extend 的 for 循环中也无法验证，即使从 ensures if old(size) + 1 == old(capacity) then fresh(buffer) else !fresh(buffer) && buffer == old(buffer) 中可以清楚地看出缓冲区的内存在整个过程中都没有改变前缀。

我觉得这可以通过归纳引理来解决，但是虽然我理解引理的形式，但我缺乏应用和推导它们的能力。

Answer 1

正在添加

invariant fresh(arr.buffer)

for 循环似乎可以修复它。那是你想要的吗？

Dafny - 循环调用时违反修改

Dafny - Violating Modifies when Calling in Loop

dynamic-arrays