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,
EDIT: ensures m == old(m)
would always be useless because a map is a value type)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])
{}
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-mapsAlso 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.