时间戳

首页 > 解决方案 > Dafny：没有找到触发条件和随之而来的断言错误

dafny - Dafny：没有找到触发条件和随之而来的断言错误

问题描述

这是我为返回两个整数的最大值的方法编写的代码：

predicate greater(x: int, a: int, b: int){
    (x >= a) && (x >= b)
}

method Max(a: int, b: int) returns (max: int)
    ensures max >= a
    ensures max >= b
    ensures forall x /*{:trigger greater(x,a,b)}*/ :: (greater(x,a,b)) ==> x >= max
{
    if (a > b){
        max := a;
    }else{
        max := b;
    }
//  assert greater(max, a, b); - trivial assertion
}

method Main(){
    var res:= Max(4, 5);

    assert res == 5;
}

如您所见，我已经尝试了Wiki 页面中提到的两种技术（手动触发器分配以及在方法主体中添加一个琐碎的无用断言。但是，我仍然收到断言错误。

我不知道还能做什么。我已经阅读了其他类似的答案，这个和这个，但到目前为止没有一个对我有帮助。

PS：我知道有一种更简单的方法可以为这种特定方法编写后置条件，但是，我真的希望仅根据 forall 量词来建模后置条件。

标签： dafny

解决方案

让我们暂时忘记greater，看看你想要实现的目标。在调用Maxin之后Main，您知道以下内容（来自 的后置条件Max）：

res >= 4
res >= 5
forall x :: x >= 4 && x >= 5 ==> x >= res

你试图以此证明res == 5。这三件事中的第二件事立即给了你一半的平等，所以你需要做的就是获得5 >= res。如果你用5for实例化量词x，你会得到

5 >= 4 && 5 >= 4 ==> 5 >= res

这简化为5 >= res，这是您所需要的，因此您的证明到此结束。

总之，证明归结为用5for实例化量词x。接下来，您需要了解一下 Dafny 验证器如何实例化量词。本质上，它通过查看量词的“形状”并在您要证明的内容的上下文中寻找类似的东西来做到这一点。我所说的“形状”是指“它使用的函数和谓词”之类的东西。通常，这种技术效果很好，但在你的情况下，量词是如此简单，以至于它没有任何“形状”可言。因此，验证者无法提出所需的实例化。

如果我们可以说“嘿，尝试用5for实例化那个量词”会很好x。好吧，我们可以，如果我们给量词一些我们可以参考的“形状”。这就是那些 wiki 和其他指南想要表达的意思。这是引入谓词的有用之处greater。（不要尝试手动编写触发器注释。）

好吧，在介绍之后greater，你的规范说

ensures greater(max, a, b)
ensures forall x :: greater(x, a, b) ==> x >= max

这表示“max满足greater(max, a, b)”和“在所有x满足的值中greater(x, a, b)，max最小的”。在调用Maxin之后Main，我们有：

greater(res, 4, 5)
forall x :: greater(x, 4, 5) ==> x >= res

回想一下，我说过验证器试图通过查看量词并查看断言周围的上下文来找出量词实例化，并且您正在尝试使用5for实例化量词x。因此，如果您可以在诱使验证者进行该实例化的断言之前向上下文添加一些内容，那么您就完成了。

答案是：你想引入greater(5, 4, 5). 它的形状很像greater(x, 4, 5)量词中的 。由于这种相似性，验证者将用 实例化x，5这给出

greater(5, 4, 5) ==> 5 >= res

并且由于greater(5, 4, 5)很容易证明是true，因此需要的事实5 >= res如下。

Main所以，改变身体

var res := Max(4, 5);
assert greater(5, 4, 5);
assert res == 5;

你就完成了。验证者将证明这两个断言。第一个是微不足道的，在证明它之后，验证者可以greater(5, 4, 5)在第二个断言的证明中使用该术语。该术语触发了量词，它产生了事实5 >= res，这证明了第二个断言。

我想指出，我们试图证明的大多数量词确实已经有了一些形状。在您的情况下，引入谓词greater是为了给量词赋予一些形状。添加额外断言（此处为assert greater(5, 4, 5)）的技术是相同的，无论是否greater已经定义或作为提供形状的普通谓词引入。

推荐阅读