如何在Dafny中确保映射（Map）未发生变更？

在以下代码中，old()的4处使用均触发警告：Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect。
注：最初参考相关问题时，曾认为ensures m == old(m)因映射是值类型而无用，但后续确认：若mymap是类的字段，ensures mymap == old(mymap)在方法中是可以生效的。
同时Unchanged()也无法作用于映射，现在不知道该如何通过ensures确保映射未发生变更？

附代码：

trait A {
    var b : nat
}

lemma oldDict(m: map<A, nat>)
    ensures m == old(m)
    ensures m.Items == old(m.Items)
    ensures forall k :: k in (m.Keys + old(m.Keys)) ==> m[k] == old(m[k])
    {}

问题分析与解决方案 #

Dafny的old()关键字核心作用是捕获堆上可变对象在方法/lemma执行前的状态。而映射map在Dafny里是值类型，按值传递，这是触发警告的根本原因：

• 如果映射是方法/lemma的参数（如示例中的m），old(m)和当前的m本质是同一个值，old()在这里完全多余，自然会触发警告。这种场景下，值类型参数本身不会被“修改”（重新赋值只会生成新的映射实例，原参数不受影响），不需要用old()来确保不变。
• 如果映射是类的字段（即堆上的可变引用），old()能正常捕获字段在执行前的状态，直接用ensures mymap == old(mymap)即可，Dafny会自动校验映射的所有键值对是否完全一致，确保映射未发生变更。

另外，Unchanged()同样只作用于堆上的可变对象，所以无法用于值类型的映射。

如果你的实际需求是确保方法不会修改某个堆上的映射字段，除了ensures，还可以配合reads子句声明方法不会修改该字段所在的对象，进一步强化约束。

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