Dafny队列实现遇modifies子句错误：call might violate context's modifies clause

你遇到的call might violate context's modifies clause错误，核心原因是Enqueue方法的modifies子句未覆盖扩容后新数组的修改操作，同时DoubleSize的modifies声明存在冗余：

1. Enqueue原modifies中的fila仅指向调用方法时的旧数组实例，但DoubleSize会将this.fila替换为新创建的数组，后续Enqueue修改新数组元素时，该数组不在Enqueue的modifies声明范围内。
2. DoubleSize原modifies中的fila是冗余的——它并未修改旧数组，只是读取其元素，修改的是自己创建的局部fresh数组（此类修改无需在modifies中声明，除非是局部变量的显式修改）。

修复后的代码 #

class {:autocontract} Fila {
    var fila: array<int>;
    var head: int;
    var tail: int;

    constructor ()
        ensures Valid();
    {
        fila := new int[5];
        head, tail:= 0, -1;
    }

    predicate Valid()
        reads this
    {
        -1 <= tail < fila.Length &&
        0 <= head < fila.Length
    }

    function isEmpty(): bool
        requires Valid()
        reads this
    {
        tail == -1
    }

    method Enqueue(x: int)
    requires Valid()
    modifies this, this.fila  // 修改this对象（tail字段、允许更新fila字段），以及当前的fila数组
    ensures Valid() 
    ensures tail == old(tail) + 1
    ensures head == old(head)
    ensures fila[tail] == x
    {
        if tail + 1 == fila.Length {
             DoubleSize();        
        }
        tail := tail + 1;
        fila[tail] := x;
    }


    method DoubleSize() 
        requires Valid()
        modifies this  // 仅修改this的fila字段，局部fresh数组aux无需声明修改
        ensures Valid() 
        ensures fresh(fila)
        ensures fila.Length == old(fila.Length) * 2
        ensures tail == old(tail) && head == old(head)        
        ensures forall i :: 0 <= i < old(fila.Length) ==> fila[i] == old(fila[i])
        {
            var aux := new int[2 * fila.Length];
            var i: int := 0;
            while i < fila.Length
                invariant 0 <= i <= fila.Length
                invariant forall j :: 0 <= j < i ==> aux[j] == fila[j]
                modifies aux  // 修改局部数组，需明确声明
            {
                aux[i] := fila[i];
                i := i + 1;
            }
             fila := aux;
        }

}

method Main()
{
    var fila := new Fila();

    fila.Enqueue(2);
    
    print(fila.isEmpty());
}

关键修复点说明 #

• Enqueue的modifies调整：modifies this, this.fila
  • modifies this允许修改对象的所有字段（包括tail和fila），确保DoubleSize替换this.fila的操作合法。
  • modifies this.fila允许修改调用Enqueue时this.fila指向的旧数组元素（对应无需扩容的场景）。
  • 扩容后的新数组是DoubleSize创建的fresh对象，Dafny允许Enqueue修改它——该对象的所有权已通过this.fila转移给Enqueue，无需额外声明。
• DoubleSize的modifies调整：移除冗余的fila，仅保留modifies this，同时为局部数组aux的修改添加modifies aux声明（局部变量的修改需显式声明）。

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