达夫尼线性搜索

Question

在进行基本线性搜索时，我遇到了 Valid() 谓词错误。它似乎只有在我取消注释构造函数和数据方法上的附加 ensures 语句时才有效。也就是当我对内容很明确的时候。

当找不到该项目时，我的搜索后置条件也遇到了问题。

关于如何解决这些问题有什么建议吗？

  class Search{
    ghost var Contents: set<int>;
    var a : array<int>;

    predicate Valid()
        reads this, a;
    {
        a != null &&
        a.Length > 0 &&

        Contents == set x | 0 <= x < a.Length :: a[x]
    }

    constructor ()
        ensures a != null;
        ensures a.Length == 4;
        //ensures a[0] == 0;
        ensures Valid();
    {
        a := new int[4](_ => 0);
        Contents := {0};
        new;
    }

    method data()
        modifies this, a;
        requires Valid();
        requires a != null;
        requires a.Length == 4;
        ensures a != null;
        ensures a.Length == 4;
        // ensures a[0] == 0;
        // ensures a[1] == 1;
        // ensures a[2] == 2;
        // ensures a[3] == 3;
        ensures Valid();
    {
        a[0] := 0;
        a[1] := 1;
        a[2] := 2;
        a[3] := 3;
        Contents := {0, 1, 2, 3};
    }

    method search(e: int) returns (r: bool)
        modifies this, a;
        requires Valid();
        ensures Valid();
        ensures r == (e in Contents)
        ensures r == exists i: int :: 0 <= i < a.Length && a[i] == e
    {
        var length := a.Length - 1;

        while (length >= 0)
            decreases length;
        {
            var removed := a[length];
            if (e == removed)
            {
                return true;
            }
            length := length - 1;
        }
        return false;
    }
  }


method Main()
{
    var s := new Search();
    s.data();
}

Answer 1

这里有几个正交问题。

首先，您已经注意到 Dafny 不愿意对 Valid 中描述 Contents 的部分进行推理。这是在 Dafny 中推理集合时的常见问题。本质上，Dafny 永远 "notice" 某个东西是集合 set x | 0 <= x < a.Length :: a[x] 的成员的唯一方法是它是否已经有表达式 a[x] 位于某处。您包含额外后置条件的解决方案之所以有效，是因为它提到了很多 a[x] 形式的表达式。另一种解决方案是将这些事实包括为断言而不是后置条件：

// in data()
assert a[0] == 0;
assert a[1] == 1;
assert a[2] == 2;
assert a[3] == 3;

其次，Dafny 无法证明您的 search 过程满足其后置条件。您需要一个循环不变量来跟踪搜索的进度。有关如何设计循环不变量的更多信息，请参阅 guide。

第三，Dafny 报告了您的 Main 关于修改条款的问题。您可以通过向 constructor 添加后置条件 fresh(a) 来解决此问题。这里的问题是 data 方法声称要修改 a，但 Dafny 无法判断 a 是否对调用者可见。

达夫尼线性搜索

Dafny linear search

dafny