Dafny循环调用push_back触发modifies子句违反错误解决咨询

• 核心报错根源：Dafny的循环默认拥有空的modifies集合，即默认不允许修改任何堆上的对象/字段。你没有给for循环显式声明允许修改的内容，调用会修改Vector字段和数组内容的push_back自然会触发modifies clause违反错误，和你是否加sameBuffer谓词无关。
• push_back的modifies子句设计不规范：原声明modifies this粒度太粗，虽然逻辑上不算错，但你去掉this后没有把push_back实际修改的thiscapacity、thisbuffer字段补上，自然会在调用同样会修改字段的extend_buffer时报错。
• 新增的sameBuffer@L(arr)不变量本身逻辑不成立：你的循环会执行16次（初始capacity为16，循环范围是0到15），第16次调用push_back时会触发扩容，buffer会被替换为新的数组，这时候必然不满足和初始buffer相等的条件，所以这个不变量不可能保持到循环结束。

1. 首先修正push_back的modifies子句，显式列出所有实际会修改的内容，原有ensures和实现逻辑保持不动即可：

method push_back(value:T)
requires Valid()
// 原有ensures子句全部保留
modifies this`size, this`capacity, this`buffer, this.buffer
{
  // 原有实现全部保留
}

2. 给for循环补充modifies子句和缺失的不变量，让Dafny明确循环允许修改的范围，以及size和循环变量的对应关系：

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

    for i : int := 0 to arr.capacity - 1
    modifies arr`size, arr`capacity, arr`buffer, arr.buffer // 显式声明循环允许修改的内容
    invariant arr.Valid()
    invariant arr.size == i // 明确size和循环变量的对应关系，帮助Dafny推导扩容触发时机
    {
        arr.push_back(oracleValue);
    }
}

3. 如果你需要验证前15次调用确实没有触发扩容，可以额外加一个分支式的不变量：

invariant if i < old(arr.capacity) then arr.buffer == old@L(arr.buffer) else true

如果想要进一步简化验证，可以把push_back的ensures子句中重复的fresh(buffer)相关判断合并为一行，减少Dafny的重复推导开销。

内容的提问来源于stack exchange，提问作者twhatm9