我正在研究自动化软件验证的要求，即一个接受代码的程序(用 C 和 Java 等语言编写的普通程序代码)，生成一堆定理，说每个循环最终都必须停止，不会违反任何断言，永远不会取消对空指针等的引用，然后将其传递给定理证明器以证明它们实际上是正确的(或者找到指示代码中错误的反例)。
问题是使用什么样的逻辑。两个主要职位似乎是:
问题是，这两个职位似乎都有很多支持。那么哪个是正确的呢？如果是第二个，是否有任何可用的示例来说明您想要做的事情，即基于一阶逻辑的验证器有问题？
最佳答案
您可以在 FOL 中完成所需的一切工作，但需要做很多额外的工作 - 很多!大多数现有系统是由没有很多时间的学者/人开发的，因此他们倾向于走捷径以节省时间/精力，因此被 HOL、函数式语言等所吸引。 但是，如果您想构建一个系统将被数十万人使用，而不仅仅是数百人，我们相信 FOL 是要走的路，因为它更容易被更广泛的受众使用。做这项工作是无可替代的。我们已经在这里工作了 25 年!请看一下我们的项目 (http://www.manmademinions.com)
问候，亚伦。
关于软件验证逻辑，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/3902684/