dafny - Dafny 断言语句是否具有效力？

我阅读文献的理解是，断言语句只是为了让用户能够看到验证者在某一点上的想法。但是根据我自己的经验，我已经看到，在引理的情况下，断言语句实际上发生了变化了验证者的想法并允许证明引理。

谁能澄清一下？

谢谢

标签： dafny

是的，添加断言语句可以帮助 Dafny 证明引理，这通常是程序员指导 Dafny 的证明搜索的方式。特别是，Dafny 可能能够证明给定的中间语句，并且它可能能够使用该语句来证明所需的引理，但它不知道在没有程序员提供的情况下查找该语句。

使用 Dafny 的经验有助于建立对什么样的断言对 Dafny 有帮助的直觉。（我建议阅读触发器，这将阐明 Dafny 证明搜索的工作原理。触发器是 Dafny 用作提示知道何时实例化量化变量的模式；使用断言来指导 Dafny 的艺术通常是找到正确的触发器。）