Dafny中修改类数组成员拆分方法后无法验证的问题咨询

我在Dafny中尝试修改类的数组成员，操作包括重新赋值数组成员、修改数组元素或两者兼具。

示例类定义如下：

class Class {
    var arrayMember : array<int>
}

下面这个方法可以通过验证，它同时包含数组成员重赋值和元素修改操作：

method verifies(obj : Class)
modifies obj, obj.arrayMember
{
    if (obj.arrayMember.Length < 5) {
        obj.arrayMember := new int[5](i => 0);
    }
    obj.arrayMember[4] := 3;
}

但当我把数组重赋值的逻辑抽成单独方法后，出现了验证问题：

method expandArray(obj : Class, size : nat)
modifies obj
ensures obj.arrayMember.Length >= size
{
    if (obj.arrayMember.Length < size) {
        obj.arrayMember := new int[size](i => 0);
    }
}

method doesNotVerify(obj : Class)
modifies obj, obj.arrayMember
{
    expandArray(obj, 5);
    obj.arrayMember[4] := 3;
}

具体来说，obj.arrayMember[4] := 3 这行无法通过验证，报错信息为：assignment might update an array element not in the enclosing context's modifies clause。我原本认为这个操作应该被允许，因为obj.arrayMember已经包含在当前方法的modifies子句中。而且把expandArray方法内联后代码又能正常验证，所以我推测问题出在expandArray方法上。

问题原因 #

问题的核心在于Dafny的modifies子句和方法契约的跟踪逻辑：

• 在doesNotVerify方法的modifies子句里，声明要修改的是调用expandArray之前的那个obj.arrayMember数组对象。
• 但expandArray方法会执行obj.arrayMember := new int[size](...)，这会把obj.arrayMember指向一个全新的数组对象。
• 对Dafny验证器而言，这个新数组并没有被包含在doesNotVerify方法的modifies声明里——你声明要修改的是旧数组，而非新创建的那个。
• 内联代码时，验证器能看到完整流程，自动将新数组纳入修改范围；但抽成独立方法后，验证器只能通过expandArray的契约推断，而当前expandArray的契约没有告知验证器：它可能替换obj.arrayMember为新数组，且这个新数组的元素可被调用者修改。

修复方案 #

需要给expandArray补充更精确的契约，明确它可能替换obj.arrayMember，并让验证器知晓新数组的修改权限可传递给调用者：

方案一：新增契约明确数组替换逻辑

method expandArray(obj : Class, size : nat)
modifies obj
ensures obj.arrayMember.Length >= size
// 明确方法可能将obj.arrayMember替换为新数组，或保持原数组不变
ensures fresh(obj.arrayMember) || old(obj.arrayMember) == obj.arrayMember
{
    if (obj.arrayMember.Length < size) {
        obj.arrayMember := new int[size](i => 0);
    }
}

方案二：直接在modifies子句中包含obj.arrayMember

method expandArray(obj : Class, size : nat)
modifies obj, obj.arrayMember
ensures obj.arrayMember.Length >= size
{
    if (obj.arrayMember.Length < size) {
        obj.arrayMember := new int[size](i => 0);
    }
}

修改后，doesNotVerify方法里的数组元素赋值就能通过验证——验证器现在明确expandArray可能替换数组，且新数组的修改权限已被契约覆盖。

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