Dafny 前置条件 0 <= size < capacity 可能不成立答案

【问题标题】：Dafny precondition 0 <= size < capacity might not holdDafny 前置条件 0 <= size < capacity 可能不成立
【发布时间】：2021-12-30 01:31:33
【问题描述】：

我是 Dafny 的新手，我试图弄清楚为什么这不起作用。我想要做的是在我的数组中插入 2 个值，priorities，分别为values。我有以下代码：

class Queue<V> {
    var size: int;
    ghost var capacity: int;
    var priorities: array<int>;
    var values: array<V>;

    predicate Valid()
    reads this
    {
        0 <= size <= capacity &&
        capacity == priorities.Length &&
        capacity == values.Length
    }

    constructor(aCapacity: int, defaultValue: V)
    requires aCapacity >= 0
    ensures Valid()
    {
        size := 0;
        values := new V[aCapacity](i => defaultValue);
        priorities := new int[aCapacity];
        capacity := aCapacity;
    }

    method insertValues(priority: int, value: V)
    modifies this.values, this.priorities, this
    requires Valid()
    requires 0 <= size < capacity  // here is the problem
    ensures Valid()
    ensures capacity == values.Length && capacity == priorities.Length
    {
        this.values[size] := value;
        this.priorities[size] := priority;
        size := size + 1;
    }
}

method Main() {
    var queue := new Queue<int>(10, 0);
    queue.insertValues(1, 10);
    queue.insertValues(2, 11);
}

但是当我尝试在 Main 中测试我的方法 insertValues 时，它会说

call may violate context's modifies clause
A precondition for this call might not hold.

前提是0 <= size < capacity。提前谢谢你。

【问题讨论】：

标签： arrays insert dafny preconditions

【解决方案1】：

问题在于 Dafny 单独分析每种方法，仅使用其他方法的规范。请参阅Dafny FAQ 了解更多信息。

您需要添加更多后置条件来保证insertValues 不会更改某些内容，并且还需要向构造函数添加更多后置条件，以便调用者知道初始状态。这是一个可以验证的版本：

class Queue<V> {
    var size: int;
    ghost var capacity: int;
    var priorities: array<int>;
    var values: array<V>;

    predicate Valid()
    reads this
    {
        0 <= size <= capacity &&
        capacity == priorities.Length &&
        capacity == values.Length
    }

    constructor(aCapacity: int, defaultValue: V)
    requires aCapacity >= 0
    ensures Valid()
    ensures fresh(priorities) && fresh(values)
    ensures size == 0 && capacity == aCapacity
    {
        size := 0;
        values := new V[aCapacity](i => defaultValue);
        priorities := new int[aCapacity];
        capacity := aCapacity;
    }

    method insertValues(priority: int, value: V)
    modifies this.values, this.priorities, this
    requires Valid()
    requires 0 <= size < capacity  // here is the problem
    ensures Valid()
    ensures capacity == old(capacity) && size == old(size) + 1 && values == old(values) && priorities == old(priorities)
    {
        this.values[size] := value;
        this.priorities[size] := priority;
        size := size + 1;
    }
}

method Main() {
    var queue := new Queue<int>(10, 0);
    queue.insertValues(1, 10);
    queue.insertValues(2, 11);
}

【讨论】：