时间戳

首页 > 解决方案 > Dafny 检查地图包含值

dafny - Dafny 检查地图包含值

问题描述

我有一张像map<int,char>dafny 这样的地图，我想看看它是否包含一些价值。

假设在 dafny 中还没有这个语法，我已经开始为它创建一个方法，但被卡住了。到目前为止，我的代码如下：

method containsValue(m: map<int,char>, val: char) returns (b: bool) 
    ensures b <==> exists i :: i in m && m[i] == val;
  {
    var i := 0;
    while (i < m.Length) {
        if (m[i] == val) 
          { return true; }      
      }
        return false;
    }

这不起作用，因为我不知道如何找到地图的大小，并且可能还有其他一些问题。请帮忙

标签： dafny

解决方案

Modern Dafny 有内置语法，使用地图的特殊.Values字段，它返回地图中的值集。Maps 也有一个.Keys用于返回键集的方法。（不幸的是，目前两者.Keys都.Values没有记录。我们正在努力。）

您可以在一行中表达您的方法，如下所示

method containsValue(m: map<int,char>, val: char) returns (b: bool) 
    ensures b <==> exists i :: i in m && m[i] == val;
{
    return val in m.Values;
}

Dafny 自动验证其是否满足其规范。

您还可以手动迭代地图的元素，如下所示

method containsValue(m: map<int,char>, val: char) returns (b: bool)
    ensures b <==> exists i :: i in m && m[i] == val;
{
    var m' := m;
    while m'.Keys != {}
        invariant m'.Keys <= m.Keys
        invariant forall k | k in m' :: m'[k] == m[k]
        invariant (exists i :: i in m && m[i] == val) ==> (exists i :: i in m' && m'[i] == val)
        decreases m'.Keys
    {
        var k :| k in m';
        if m'[k] == val {
            return true;
        }
        m' := map k' | k' in m' && k' != k :: m'[k'];
    }
    return false;
}

Dafny 的地图解析和内置语法通常使这种迭代变得不必要，因此是不好的风格。（特别是对于这种方法，单行版本更清晰。）但是，它偶尔在其他情况下有用，因此了解该技术是件好事。

推荐阅读