"Some instances of this call cannot safely be inlined."

Question

在 Dafny 中，错误消息 "Some instances of this call cannot safely be inlined" 是什么意思？

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

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

Answer 1

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

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

您可以将发生的事情想象成，本质上，将谓词的主体内联到谓词的调用站点。但是，有时无法做到这一点。例如，如果谓词是递归的，那么这种内联必须有一些限制。如果无法进行内联，则意味着您收到的任何错误消息只会说 "can't prove 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 );

鲁斯坦

"Some instances of this call cannot safely be inlined."

"Some instances of this call cannot safely be inlined."

dafny