lemma与ghost method的区别是什么？调用报错问题咨询

核心语义差异 #

• Lemma：本质是逻辑证明里的「定理/引理」，专门用来表达某个确定为真的逻辑断言，全程服务于形式化证明的推导逻辑，不会涉及任何状态修改，也没有副作用。
• Ghost Method：属于「幽灵代码」范畴，虽然不影响程序运行时行为，但它的语义更贴近普通方法——可以包含幽灵变量的修改、流程控制，甚至调用其他幽灵方法，主要用来封装辅助建模的逻辑，而非直接表达逻辑真值。

证明上下文的调用限制 #

在Dafny这类形式化验证工具中，像lemma里的calc块这种证明上下文，对可调用的代码有严格限制：只能调用同为逻辑证明构件的lemma。因为这类上下文的核心是构建严谨的逻辑推导链，而ghost method可能包含状态操作，无法被证明系统安全地纳入推导过程。

你的报错原因 #

你代码里的calc块是用来构建等式推导的证明环节，这里只允许调用lemma来辅助推导。而foo是ghost method，哪怕它是幽灵代码，也不符合证明上下文的调用规则，所以才会抛出in a hint, calls are allowed only to lemmas错误。

如果想在lemma里复用这段逻辑，最直接的解决办法是把foo改成lemma；要是foo必须处理幽灵状态修改这类lemma做不到的操作，那得调整证明结构——比如先调用ghost method，再用断言把结果固定下来，再把断言纳入calc的推导中。

内容的提问来源于stack exchange，提问作者mazin