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