Example about Maps from Tutorial cause assertion violation

Dec 8, 2014 at 12:52 PM
The below code snippet is one of the examples from the Dafny tutorial on value types illustrating how to remove an entry from a map. (http://www.rise4fun.com/Dafny/tutorial/ValueTypes).

However, one of my students brought to my attention that this example appears to be buggy, it gives me an assertion violation.

method test() {
var m := map[3 := 5, 4 := 6, 1 := 4];
var l := map i | i in m && i != 3 :: m[i];
assert l == map[4:= 6, 1 := 4];
}

Furthermore, we've recently had quite a bit of trouble using Dafny at rise4fun for the course I'm teaching, as it has been very slow or sometimes not responding at all. As the web interface is nicer to use for teaching purposes than a terminal, I hope those issues can be straightened out.
Dec 9, 2014 at 4:05 PM
Edited Dec 10, 2014 at 1:51 PM
I think this is something funky to do with matching in Z3. My guess is that the way that Dafny implements the map comprehension somehow makes the value (map i | i in m && i != 3 :: m[i]) unsuitable for use in the SMT solver's e-graph (or perhaps it is suitable, but Dafny does not give an appropriate trigger). And the usual way to fix these kinds of problems is to introduce a function, so that Z3 has something it can use in the e-graph in place of the value map i | i in m && i != 3 :: m[i]. The following appears to work:
function method RemoveElementFromMap(m:map<int,int>, x:int) : map<int,int>
{
  map i | i in m && i != x :: m[i]
}

method test() {
  var m := map[3 := 5, 4 := 6, 1 := 4];
  var l := RemoveElementFromMap(m,3);
  assert l == map[4:= 6, 1 := 4];
} 
http://rise4fun.com/Dafny/lmquH

It is possible my explaination is wrong. We could probably work out the exact reason by looking in detail at what Boogie code is generated by Dafny for this example.