在Dafny中，错误消息"此调用的某些实例无法安全地内联"是什么意思？
我看到它报告了对断言内部谓词的调用。 例如
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 );
鲁斯坦