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

Question

我正在尝试编写一个具有固定大小数组的愚蠢程序。如果这个数组还没有被填充并且被添加的值在数组中不存在，那么可以通过一个方法添加它。起初它似乎运行很好，但是，当我调用该方法超过 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 class 的说明揭示了 Test 对象的内部表示的所有内容。如果您可以向调用者隐藏这些详细信息，通常最终会隐藏更多信息、更好的规范以及更好的证明者性能。为此，您需要添加一个对象不变性（在 Dafny 中惯用地编码为 Valid() 谓词）。我会有很多东西要解释。但我看到您已经在使用 {:autocontracts}，所以您可能对此有所了解。因此，在没有进一步解释的情况下，这里是您的 class 的规范以更抽象的形式看起来的样子。

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 语句来验证程序。

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

Method precondition fails after 4 calls to the method - Value uniqueness in array

arrays

dafny