2

在进行基本线性搜索时，我的 Valid() 谓词出现错误。它似乎仅在我取消注释构造函数和数据方法上的附加确保语句时才有效。也就是说，当我对内容非常明确时。

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

关于如何解决这些问题的任何建议？

  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();
}
4

1 回答 1

0

这里有几个正交问题。

首先，您已经注意到 Dafny 不愿意对Valid描述的部分进行推理Contents。这是在 Dafny 中推理集合时的常见问题。本质上，达夫尼“注意到”某物是该集合成员的唯一方法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程序满足其后置条件。您需要一个循环不变量来跟踪搜索的进度。有关如何设计循环不变量的更多信息，请参阅指南。

第三，Dafny 报告了Main关于修改子句的问题。您可以通过fresh(a)向constructor. 这里的问题是该data方法声称要 modify a，但 Dafny 无法判断a调用者是否可以看到。

于 2017-11-06T20:05:50.380 回答