Search code examples
dafny

Ensure that a map didn't change?

In the following code, all 4 times that old() appears, it triggers this warning:
Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect.

(Additionally, according to another question, ensures m == old(m) would always be useless because a map is a value type) EDIT: ensures mymap == old(mymap) does work in methods. Makes sense when mymap is a field in the containing class.

Unchanged() doesn't work with maps either. So I've run out of ideas. How can one ensure that a map didn't change?

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])
    {}
Solution

  • As it mentions it is a value type, it won't change if you return the same map. You have to create another map to create a map that is not equal to the original. When you do an update to a map like m[k := v] you are actually creating a new map which you must reassign to a variable otherwise the change will not be preserved. https://dafny.org/dafny/DafnyRef/DafnyRef#sec-maps

    Also to write lemmas about frames you need to use a twostate lemma. There aren't many examples but the blog has some good examples here.