1

我正在尝试在 dafny 中创建一个谓词，以确定字符数组是否包含任何重复项。它最终应该测试以下内容：对于数组中的任何两个元素，如果 theor 值相等，则它们的索引也必须相等。请忽略少于2个元素的情况

predicate noDuplicates (a:array<char>)
requires a!= null
reads a
{
forall j,k:: (0<=j<a.Length && 0<=k<a.Length) ==> ((a[j]==a[k]) ==> (j==k))
}

但是，当我运行以下测试时，断言失败。为什么会这样？

var b: array<char> := new char[5];
b[0], b[1], b[2], b[3], b[4] := 't', 'e', 's', 't', 's';
assert noDuplicates(b) == false;
4

1 回答 1

0

我认为问题在于求解器图中没有任何内容可供 dafny 实例化量词。您可以通过添加额外的断言来验证它，以便 Dafny 得到使用这些值来实例化量词的想法。

例如这个：

method Main() {
    var b: array<char> := new char[5];
    b[0], b[1], b[2], b[3], b[4] := 't', 'e', 's', 't', 's';
    assert b[0] == 't';
    assert b[3] == 't';
    assert noDuplicates(b) == false;
}

或这个

method Main() {
    var b: array<char> := new char[5];
    b[0], b[1], b[2], b[3], b[4] := 't', 'e', 's', 't', 's';
    assert b[0] == b[3];
    assert noDuplicates(b) == false;
}

为什么这有效

通常当 Dafny 需要证明涉及量词的东西时，它必须选择值来实例化量词（由于减少到 SAT）。它通常会尝试的一件事是一个新的任意常数，但这不会让你走得太远。您需要它来选择值 0 和 3（例如）。然而，有很多整数，所以随机选择这些值的机会很低——低到实际上它甚至不会尝试。相反，它所做的是查看它已经知道的任何事实，并挑选出任何与量化公式中原子形状相匹配的事实。在这种情况下，它正在寻找类似的东西a[i]==a[j] - 所以通过放入涉及b[0]和的断言，b[3]这会促使 Dafny 最终尝试值0和3fori和j. 直接版本b[0]==b[3]非常直接地工作，而间接版本b[0]==t && b[3]==t将间接导致 Dafny 在其 egraph 之间b[0]和中放置边缘b[3]并推断出事实b[0]==b[3]，这将促使它尝试0并3实例化量词。

我很想知道任何其他解决方案。

编辑

我想到了另一个使用fuelannotation的解决方案，但我不知道它是否真的是一个更好的解决方案：

method Main() {
  var b: array<char> := new char[5];
  b[0], b[1], b[2], b[3], b[4] := 't', 'e', 's', 't', 's';
  assert {:fuel contains,3} noDuplicates(b[..]) == false;
}

predicate noDuplicates (a:seq<char>)
{
   a == [] || (!contains(a[1..], a[0]) && noDuplicates(a[1..])) 
}

predicate  contains (a:seq<char>, v:char)
{
  a != [] && (a[0] == v || contains(a[1..],v)) 
}
于 2016-05-10T22:05:31.917 回答