时间戳

首页 > 解决方案 > “此调用的某些实例无法安全地内联。”

dafny - “此调用的某些实例无法安全地内联。”

问题描述

在 Dafny 中，错误消息“无法安全地内联此调用的某些实例”是什么意思？

我看到它报告了对断言内部谓词的调用。例如

   assert LessThanOrEqual( [a[z]], a[z+1..r] ) ;

标签： dafny

解决方案

这是一条信息性消息（不是错误），而且相当晦涩！（我必须自己查一下才能理解。）

当存在涉及谓词的证明义务时（此处LessThanOrEqual），Dafny 验证器会在内部进行设置，以便如果它无法证明谓词，它将能够告诉您谓词主体内的哪个合取失败。您将看到这是伴随错误消息的“关联声明”消息。

本质上，您可以将发生的事情视为将谓词的主体内联到谓词的调用站点中。然而，有时这是无法做到的。例如，如果谓词是递归的，那么这种内联必须有一些限制。如果无法进行内联，则意味着您收到的任何错误消息只会说“无法证明LessThanOrEqual(...)”，但它不会告诉您它的定义的哪一部分LessThanOrEqual无法证明。

不能进行内联的一个更微妙的原因涉及量词。验证器通过所谓的匹配触发器与量词一起工作。当实例化量词是一个好主意时，触发器会通知验证者。关于什么可以和不能成为触发器有一些规则。在您的示例中相关的一个规则是算术+不能成为触发器的一部分。我猜你的定义LessThanOrEqual涉及一个量词，并且验证者选择作为该量词的触发器的一个术语涉及到LessThanOrEqual. 如果上面的调用LessThanOrEqual是内联的，那么+就会潜入触发器，这是规则不允许的。

因此，Dafny 选择不将此调用内联到LessThanOrEqual. 所有这一切意味着如果验证者未能证明断言，您将获得稍微不太精确的错误位置。您可能不会注意到或对此感到困扰；事实上，得到一个不太精确的错误消息可能比你得到的信息性消息更令人费解。

有一种方法可以抑制信息性消息：如果您传入一个不直接提及的等效表达式+。例如，您可以使用局部变量：

ghost var s := a[z+1..r];
assert LessThanOrEqual( [a[z]], s );

或 let 表达式：

assert var s := a[z+1..r]; LessThanOrEqual( [a[z]], s );

鲁斯坦

推荐阅读