Dafny反向查找图

Question

嗨，我有一个像map<char,int>的地图，我想做一个反向查找，也就是从一个值中找到一个键。

在Dafny (例如map.getKey(value))中，是否有任何方法可以做到这一点，而Dafny还没有文档化？

我认为一种解决方案可以是逆映射，这样我就可以将map<char,int>反转到map<int,char，然后使用反转映射上的正常查找。我不知道如何做到这一点，但已经尝试使用map table[i] | i in table :: i通过地图理解，但这是行不通的。

请帮帮我。

Answer 1

你可以用一个“让这样-那个”的语句来做到这一点。例如：

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...
}

您也可以按如下方式倒置地图(但您不需要只进行一次反向查找)

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
}