在 Dafny 中验证 Max 函数时违反断言？答案

【问题标题】：assertion violation when verifying Max function in Dafny?在 Dafny 中验证 Max 函数时违反断言？
【发布时间】：2018-10-10 08:30:55
【问题描述】：

以下程序导致assert v==40 上的断言冲突：为什么？当数组a只包含一个元素时，程序可以被验证。

method Max(a:array<int>) returns(max:int)
requires 1<=a.Length
ensures forall j:int :: 0<=j< a.Length ==> max >= a[j]
ensures exists j:int :: 0<=j< a.Length &&  max == a[j]
{
   max:=a[0];
   var i :=1;
   while(i < a.Length)
   invariant 1<=i<=a.Length
   decreases a.Length-i
   invariant forall j:int :: 0<=j<i ==> max >= a[j]
   invariant exists j:int :: 0<=j<i &&  max == a[j]
   {
     if(a[i] >= max){max := a[i];}
     i := i + 1;
   }
}
method Test(){
   var a := new int[2];
   a[0],a[1] := 40,10;
   var v:int:=Max(a);
   assert v==40;
}

【问题讨论】：

标签： dafny

【解决方案1】：

这确实很奇怪！这归结为 Dafny 处理量词的方式。

让我们从一个人类级别的证据开始，证明该断言实际上是有效的。从Max 的后置条件，我们知道v 的两件事：（1）它至少和a 中的每个元素一样大，以及（2）它等于a 的某个元素。根据 (2)，v 是 40 或 10，根据 (1)，v 至少为 40（因为它至少与 a[0] 一样大，即 40）。由于10至少不是40，v不可能是10，所以一定是40。

现在，为什么 Dafny 无法自动理解这一点？这是因为 (1) 中的 forall 量词。 Dafny（实际上是 Z3）在内部使用“触发器”来近似全称量词的行为。（在没有任何近似的情况下，使用量词进行推理通常是无法确定的，因此需要像这样的一些限制。）触发器的工作方式是，对于程序中的每个量词，都会推断出称为触发器的句法模式。然后，除非触发器匹配上下文中的某个表达式，否则该量词将被完全忽略。

在本例中，事实 (1) 的触发器为 a[j]。（您可以通过将鼠标悬停在量词上来查看在 Visual Studio 或 VSCode 或 emacs 中推断出哪些触发器。或者在命令行上，通过传递选项 /printTooltips 并查找行号。）这意味着量词将被忽略除非上下文中存在a[foo] 形式的某些表达式，否则对于任何表达式foo。然后 (1) 将用foo 实例化为j，我们将学习max >= a[foo]。

由于您的Test 方法的断言没有提及a[foo] 形式的任何表达式，Dafny 将根本无法使用事实（1），这会导致虚假断言违规。

修复Test 方法的一种方法是添加断言

assert v >= a[0];

就在另一个断言之前。这是我们在人类水平证明中需要的事实 (1) 的关键结果，它包含与触发器匹配的表达式a[0]，允许 Dafny 实例化量词。其余的证明会自动进行。

有关一般触发器以及如何手动编写触发器的更多信息，请参阅this answer。

【讨论】：