arrays - 方法前提条件在 4 次调用方法后失败 - 数组中的值唯一性

Question

我正在尝试编写一个具有固定大小数组的 dafny 程序。如果该数组尚未填充并且要添加的值尚不存在于数组中，则可以通过方法添加该数组。起初它似乎运行良好，但是，当我调用该方法超过 4 次时，我收到错误

SimpleTest.dfy(37,15): Error: A precondition for this call might not hold.
SimpleTest.dfy(17,23): Related location: This is the precondition that might not hold.
Execution trace:
    (0,0): anon0

它突出显示了下面 MCVE 中的 requires x !in arr[..] 行。

为什么一旦调用该方法四次以上，前提条件就会开始失败？无论数组的固定大小有多大，似乎都会发生

class {:autocontracts} Test
{
    var arr: array<nat>;
    var count: nat;

    constructor(maxArrSize: nat)
        requires maxArrSize > 1
        ensures count == 0
        ensures arr.Length == maxArrSize
        ensures forall i :: 0 <= i < arr.Length ==> arr[i] == 0
    {
        arr := new nat[maxArrSize](_ => 0);
        count := 0;
    }

    method AddIn(x: nat)
        requires x !in arr[..]
        requires x > 0
        requires 0 < arr.Length
        requires count < arr.Length
        ensures arr[..] == old(arr[.. count]) + [x] + old(arr[count + 1 ..])
        ensures count == old(count) + 1
        ensures arr == old(arr)
    {
        arr[count] := x;
        count := count + 1;
    }
}

method Main()
{
    var t := new Test(20);
    t.AddIn(345);
    t.AddIn(654);
    t.AddIn(542);
    t.AddIn(56);
    t.AddIn(76);
    t.AddIn(8786);
    print t.arr[..];
    print "\n";
    print t.count;
    print " / ";
    print t.arr.Length;
    print "\n";
}

Answer 1

为了证明该方法的前置条件，验证者必须经历很多情况，每个情况都使用了堆、序列和构造函数后置条件中量词的属性。这些情况似乎耗尽了验证器的某些限制，因此您会收到一个错误，表明它无法证明某些内容。

您可以通过编写一些断言来帮助验证者。这些断言还将确认您对程序正在构建的程序状态的理解。例如，如果您添加这些 assert 语句，验证程序既会确认断言，又能够证明您的整个程序。

method Main()
{
  var t := new Test(20);
  assert t.arr[..] == seq(20, _ => 0);
  t.AddIn(345);
  assert t.arr[..] == [345] + seq(19, _ => 0);
  t.AddIn(654);
  assert t.arr[..] == [345, 654] + seq(18, _ => 0);
  t.AddIn(542);
  assert t.arr[..] == [345, 654, 542] + seq(17, _ => 0);
  t.AddIn(56);
  assert t.arr[..] == [345, 654, 542, 56] + seq(16, _ => 0);
  t.AddIn(76);
  assert t.arr[..] == [345, 654, 542, 56, 76] + seq(15, _ => 0);
  t.AddIn(8786);
  assert t.arr[..] == [345, 654, 542, 56, 76, 8786] + seq(14, _ => 0);
  print t.arr[..];
  print "\n";
  print t.count;
  print " / ";
  print t.arr.Length;
  print "\n";
}

您不需要所有这些断言，但我将它们留在这里，以便您可以看到一般形式。

一切都通过这些附加断言进行验证的原因是，每个断言都可以很容易地从前一个断言中得到证明。因此，额外的断言会引导验证者更快地提供证明(特别是，引导验证者在放弃之前找到证明)。

顺便说一句，您对 Test 类的规范揭示了有关 Test 对象内部表示的所有内容。如果您可以对调用者隐藏这些详细信息，那么您通常会获得更多的信息隐藏、更好的规范以及更好的证明器性能。为此，您需要添加一个对象不变量(在 Dafny 中惯用编码为 Valid() 谓词)。我有很多事情需要解释。但我发现您已经在使用 {:autocontracts}，所以也许您对此有所了解。因此，无需进一步解释，以下是您的类的规范在更抽象的形式中的样子。

class {:autocontracts} Test
{
  // The public view of the Test object is described by the following two fields:
  ghost var Contents: seq<nat>
  ghost var MaxSize: nat
  // The private implementation of the Test object is given in terms of the
  // following fields. These fields are never mentioned in pre/post specifications.
  var arr: array<nat>
  var count: nat

  predicate Valid() {
    count <= arr.Length == MaxSize &&
    Contents == arr[..count]
  }

  constructor(maxArrSize: nat)
    ensures Contents == [] && MaxSize == maxArrSize
  {
    arr := new nat[maxArrSize];
    Contents, MaxSize, count := [], maxArrSize, 0;
  }

  method AddIn(x: nat)
    requires x !in Contents
    requires |Contents| < MaxSize
    ensures Contents == old(Contents) + [x] && MaxSize == old(MaxSize)
  {
    arr[count], count := x, count + 1;
    Contents := Contents + [x];
  }
}

method Main()
{
  var t := new Test(20);
  t.AddIn(345);
  t.AddIn(654);
  t.AddIn(542);
  t.AddIn(56);
  t.AddIn(76);
  t.AddIn(8786);
  print t.arr[..], "\n";
  print t.count, " / ", t.arr.Length, "\n";
}

请注意，在此版本中，不需要额外的 assert 语句来验证程序。