Dafny reverse lookup map

Question

Hi I have a map like map<char,int> and I wish to do a reverse lookup i.e. find a key from a value.

Is there any way to do this in Dafny (e.g. map.getKey(value)) which has not been documented yet?

I am thinking that one solution could be to inverse the map so that I could inverse a map<char,int> to map<int,char and then use the normal lookup on the inversed map. I am not sure how to do this but have tried using map table[i] | i in table :: i by map comprehension but this does not work.

Please help me.

Answer 1

You can use a "let such-that" statement to do that. For example:

method Test(m: map<char,int>, val: int)
    requires exists i :: i in m && m[i] == val;
{
    var i :| i in m && m[i] == val;
    // now use i...
}

You can also invert the map as follows (but you don't need to just to do a single reverse lookup)

function method InvertMap(m: map<char,int>): map<int,char>
{
    map b | b in m.Values :: var a :| a in m && m[a] == b; a
}