方法前置条件在对数组中的方法-Value唯一性进行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的线CCD_ 1。

为什么在方法被调用四次以上后，前置条件就会开始失败？无论的固定大小有多大，它似乎都会发生

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