Dafny 前提条件 0 <= 大小<容量可能不成立

Question

我是Dafny的新手，我试图弄清楚为什么这不起作用。我想做的是在数组中插入两个值，分别为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.

前提条件是CCD_ 4。提前谢谢。

Answer 1

问题是Dafny单独分析每个方法，只使用其他方法的规范。有关更多信息，请参阅Dafny常见问题解答。

您需要添加更多的后处理条件，以确保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);
}