dafny断言中的数组初始化失败后

Question

我正试图进入dafny，但我无法理解以下内容：

var a := new int[10];
var i := 0;
while i < 10
decreases 20 - i 
{
a[i] := i;
i := i+1;
}
assert a[5] == 5;

到目前为止，内容相当简单：声明新数组a，并用相应的索引位置初始化它的值。因此断言语句应该是真的，然而dafny抱怨道：；断言违反"；。我试着将a[5]与其他数字进行比较，例如4和6，以及其他一些非常接近的数字，但都不起作用，我想知道为什么？

与此相关，我想问打印是如何在dafny中工作的(使用VSCode(？

谢谢！

Answer 1

要了解验证器在这里失败的原因，您必须了解Dafny验证器是如何处理while循环的。简而言之，不允许验证者"；调查"；while循环的主体，当试图证明主体之外的断言时。

为了解释Dafny中的while循环，您需要应用循环不变量，教程可能比我解释得更好：https://rise4fun.com/Dafny/tutorial/Guide

我建议看Find的例子，特别是类似于你想要做的事情