Dafny反向查询图 [英] Dafny reverse lookup map

问题描述

我有一个类似 map< char，int> 的地图，我希望进行反向查找，即从一个值中找到一个键。

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.

在Dafny中有没有办法做到这一点（例如 map.getKey（value））呢？

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

我想一种解决方案是将地图反过来，这样我就可以将 map< char，int> 反过来 map< int，char ，然后在反图上使用常规查找。我不确定如何执行此操作，但是尝试使用 map表[i] |我在表中的:: ::我通过地图理解，但这不起作用。

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.

请帮助我。

推荐答案

您可以使用 let such-that语句来做到这一点。例如：

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
}

这篇关于Dafny反向查询图的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！