Dafny中multiset不变性规范下断言验证失败问题咨询

1. Dafny验证基于方法契约，而非实现代码 #

即使你的do_nothing方法体是空的，Dafny在验证test方法时，只会依据do_nothing声明的契约（modifies和ensures）来推断调用后的数组状态，完全忽略方法的实际代码逻辑。也就是说，验证器会默认do_nothing可以执行任何符合契约的修改操作——比如交换数组元素位置、将元素移动到其他索引位等，只要最终数组的multiset和原数组一致即可。

2. Multiset相等的隐含逻辑未被自动推导 #

multiset(a[..]) == multiset(old(a[..]))确实能保证修改后的数组元素种类和数量与原数组完全一致（原数组没有0，修改后的数组也不可能出现0），但Dafny的自动定理证明器不会自动完成这层逻辑推导：它无法直接从“multiset中0的计数为0”关联到“数组任意位置的元素都不为0”。这一步需要你显式提供逻辑引导，验证器才能完成断言的证明。

解决方法示例 #

你可以在调用do_nothing后添加中间断言，帮验证器建立逻辑链：

do_nothing(a);

// 显式声明：修改后的数组所有元素都属于原数组的元素集合
assert forall i: nat :: i < a.Length ==> a[i] in multiset(old(a[..]));
// 原数组不含0，因此a[0]必然不为0
assert a[0] != 0; // 此时验证通过

或者强化do_nothing的契约，直接明确数组元素的取值范围：

method do_nothing(a: array<int>)
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
  ensures forall i :: 0 <= i < a.Length ==> a[i] in multiset(old(a[..]))
{
  // nothing is done
}

修改契约后，原test方法中的断言无需额外代码即可通过验证。

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