达夫尼没有验证琐碎的断言答案

【问题标题】：Dafny not verifying trivial assertion达夫尼没有验证琐碎的断言
【发布时间】：2020-05-31 07:21:30
【问题描述】：

下面的代码，也在https://rise4fun.com/Dafny/I4wM，

function abst(bits: array<int>,low:int,high: int): int
    requires 0<=low<=high<=8
    requires bits.Length==8
    decreases high-low
    reads bits
{   if low==high
        then 0 
        else 2*abst(bits,low+1,high) + bits[low]
}

method M() {

    var byte: int;
    var bits:= new int[8];
    bits[0]:= 1;
    bits[1]:= 1;
    bits[2]:= 1;
    bits[3]:= 1;
    bits[4]:= 1;
    bits[5]:= 1;
    bits[6]:= 1;
    bits[7]:= 1;

    // assert abst(bits,2,2) == 0; // Why is this needed?
    assert abst(bits,0,2) == 3;

}

无法验证最后一行的断言。（我使用的是 Rise4Fun 的在线 Dafny。）如果前面的断言未注释，则验证成功。

我将不胜感激。谢谢！

【问题讨论】：

标签： verification assertion dafny

【解决方案1】：

Dafny 验证程序仅展开函数一次或两次。具体来说，如果该函数出现在您要证明的断言中（就像您的示例中的 abst 所做的那样），则该函数将展开两次。但是，为了证明您的断言，abst 的定义需要展开 3 次。因此，验证者无法自动证明。你必须帮助它。

当您取消注释第一个断言时，它将用于第二个断言的证明。由于第一个断言提供了您需要的 abst 的最后一个实例化，因此它有助于证明第二个断言。第一个断言本身也被证明了，但这是自动的，因为它只需要展开一次 abst。

如果把证明详细写出来，是这样的：

calc {
  abst(bits,0,2);
==  // def. abst
  2*abst(bits,1,2) + bits[0];
==  // def. abst
  2*(2*abst(bits,2,2) + bits[1]) + bits[0];
==  // def. abst
  2*(2*0 + bits[1]) + bits[0];
==  // def. bits[0] and bits[1]
  2*(2*0 + 1) + 1;
==  // arithmetic
  3;
}

在这个证明中，您可以看到所需的函数实例化。

您的应用程序中真的需要数组吗？数组在堆上分配并且是可变的（这意味着您需要reads 子句和其他复杂性）。如果您只需要一个不可变序列，那么我建议您将array<int> 更改为seq<int>。这将使事情变得更容易（再次 - 如果您不需要数组的可变特性）。此外，对于您上面的断言，它带来了另一个好处：然后您传递给abst 的所有参数都是文字。对于文字，Dafny 愿意（或多或少）无限制地展开函数。因此，您的原始断言会自动验证。

鲁斯坦

【讨论】：