我正在研究自动化软件验证的要求，即一个接收代码的程序（用 C 和 Java 等语言编写的普通程序代码），生成一堆定理，说每个循环必须最终停止，不会违反任何断言，将永远不会取消引用空指针等，然后将其传递给定理证明者以证明它们实际上是正确的（或者在代码中找到指示错误的反例）。
问题是使用什么样的逻辑。两个主要职位似乎是：
一阶逻辑就好了。
一阶逻辑不够表达，需要高阶逻辑。
问题是，这两个职位似乎都有很多支持。那么哪一个是对的呢？如果是第二个，是否有任何您想做的事情的可用示例，基于一阶逻辑的验证器有问题？
您可以在 FOL 中做所有您需要的事情，但这是很多额外的工作——很多！大多数现有系统都是由没有太多时间的学者/人开发的，因此他们倾向于走捷径以节省时间/精力，因此被 HOL、函数式语言等所吸引。但是，如果你想构建一个系统将被数十万人使用，而不仅仅是数百人，我们相信 FOL 是可行的方法，因为它更容易为更广泛的受众所接受。做这项工作是无可替代的；我们已经在这里工作了 25 年了！请看看我们的项目 (http://www.manmademinions.com)
问候，亚伦。
在我的实践经验中，似乎是“1.一阶逻辑就好了”。有关完全用基于一阶逻辑的规范语言编写的各种功能的完整规范示例，请参见示例中的ACSL或此案例研究。
一阶逻辑具有经过多年改进的自动化证明者（不是证明助手），以处理来自程序验证的井属性。用于这些用途的著名自动证明器有Simplify、Z3和Alt-ergo。如果这些证明者失败并且没有明显的引理/断言可以添加来帮助他们，您仍然可以为困难的证明义务启动证明助手。另一方面，如果您使用 HOL，则根本无法使用 Simplify、Z3 或 Alt-ergo，虽然我听说过用于高阶逻辑的自动证明器，但我从未听说过它们因其在属性方面的效率而受到称赞从节目。
我们发现 FOL 对于大多数验证条件都很好，但高阶逻辑对于少数情况来说是无价的，例如用于证明集合中元素总和的属性。所以我们的定理证明器（在 Perfect Developer 和 Escher C Verifier 中使用）基本上是一阶的，但也能够进行一些更高阶的推理。