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

Posted 2023-01-08

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

我看到它报告了在assert中调用谓词。例如：

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

答案

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

[当存在涉及谓词的证明义务时（此处为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 );

Rustan