软件验证逻辑
我正在研究自动化软件验证的要求，即一个接受代码（用 C 和 Java 等语言编写的普通程序代码）的程序，生成一堆定理，表明每个循环最终必须停止，不会违反任何断言，永远不会对空指针等进行取消引用，然后将其传递给定理证明者以证明它们实际上是正确的（或者找到一个表明代码中存在错误的反例）。
问题是使用什么样的逻辑。两个主要立场似乎是：
一阶逻辑就很好。
一阶逻辑的表达能力不够，您需要更高阶的逻辑。
问题是，这两个立场似乎都得到了很多支持。那么哪一个是正确的呢？如果是第二个，是否有任何可用的示例来说明您想要做的事情，而基于一阶逻辑的验证者却遇到了麻烦？
I'm looking at the requirements for automated software verification, i.e. a program that takes in code (ordinary procedural code written in languages like C and Java), generates a bunch of theorems saying that each loop must eventually halt, no assertion will be violated, there will never be a dereference of a null pointer etc., then passes same to a theorem prover to prove they are actually true (or else find a counterexample indicating a bug in the code).
The question is what kind of logic to use. The two major positions seem to be:
First-order logic is just fine.
First-order logic isn't expressive enough, you need higher order logic.
Problem is, there seems to be a lot of support for both positions. So which one is right? If it's the second one, are there any available examples of things you want to do, that verifiers based on first-order logic have trouble with?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
您可以在 FOL 中完成您需要的所有操作，但这需要大量额外工作 - 很多！大多数现有系统都是由学者/没有太多时间的人开发的，因此他们很想走捷径来节省时间/精力，从而被 HOL、函数式语言等所吸引。但是，如果你想构建一个如果系统将被数十万人使用，而不仅仅是数百人，我们相信 FOL 是最佳选择，因为它更容易为更广泛的受众所使用。工作是无可替代的；我们已经这样做了 25 年了！请看看我们的项目 (http://www.manmademinions.com)
问候，Aaron。
You can do everything you need in FOL, but it's a lot of extra work - a LOT! Most existing systems were developed by academics / people with not a lot of time, so they are tempted to take short cuts to save time / effort, and thus are attracted to HOLs, functional languages, etc. However, if you want to build a system that is to be used by hundreds of thousands of people, rather than merely hundreds, we believe that FOL is the way to go because it is far more accessible to a wider audience. There's just no substitute for doing the work; we've been at this for 25 years now! Please take a look at our project (http://www.manmademinions.com)
Regards, Aaron.
根据我的实践经验，似乎是“1.一阶逻辑就可以了”。有关完全使用基于一阶逻辑的规范语言编写的各种函数的完整规范的示例，请参见 ACSL 示例 或 本案例研究。
一阶逻辑具有自动证明器（不是证明助手），多年来经过改进，可以处理来自程序验证的井属性。用于这些用途的著名自动证明程序有 Simplify、Z3 和 Alt-ergo。如果这些证明者失败，并且您没有可以添加明显的引理/断言来帮助他们，您仍然可以启动证明助手来完成困难的证明义务。另一方面，如果您使用 HOL，则根本无法使用 Simplify、Z3 或 Alt-ergo，虽然我听说过用于高阶逻辑的自动证明器，但我从未听说过它们在属性方面因其效率而受到赞扬来自程序。
In my practical experience, it seems to be "1. First-order logic is just fine". For examples of complete specifications for various functions written entirely in a specification language based on first-order logic, see for instance ACSL by Example or this case study.
First-order logic has automated provers (not proof assistants) that have been refined over the years to handle well properties that come from program verification. Notable automated provers for these uses are for instance Simplify, Z3, and Alt-ergo. If these provers fail and there is no obvious lemma/assertion you can add to help them, you still have the recourse of starting up a proof assistant for the difficult proof obligations. If you use HOL on the other hand, you cannot use Simplify, Z3 or Alt-ergo at all, and while I have heard of automated provers for high-order logic, I have never heard them praised for their efficiency when it comes to properties from programs.
我们发现 FOL 对于大多数验证条件来说都很好，但高阶逻辑对于少数情况来说是无价的，例如用于证明集合中元素求和的属性。因此，我们的定理证明器（在 Perfect Developer 和 Escher C Verifier 中使用）基本上是一阶的，但也能够进行一些高阶推理。
We've found that FOL is fine for most verification conditions, but higher order logic is invaluable for a small number, for example for proving properties about summation of the elements in a collection. So our theorem prover (used in Perfect Developer and Escher C Verifier) is basically first order, but with the ability to do some higher order reasoning as well.