有没有人试过用 Z3 本身证明 Z3? [英] Has anyone tried proving Z3 with Z3 itself?

问题描述

有人试过用 Z3 本身证明 Z3 吗?

Has anyone tried proving Z3 with Z3 itself?

是否有可能使用 Z3 证明 Z3 是正确的?

Is it even possible, to prove that Z3 is correct, using Z3?

更多的理论，是否有可能证明工具 X 是正确的，使用 X 本身?

More theoretical, is it possible to prove that tool X is correct, using X itself?

推荐答案

简短的回答是:不，没有人试图使用 Z3 本身来证明 Z3":-)

The short answer is: "no, nobody tried to prove Z3 using Z3 itself" :-)

我们证明程序 X 是正确的"这句话非常具有误导性.主要问题是:正确是什么意思.在 Z3 的情况下，可以说 Z3 是正确的，至少，对于不可满足的问题，它永远不会返回sat"，对于可满足的问题，它永远不会返回unsat".可以通过还包括其他属性来改进此定义，例如:Z3 不应崩溃；Z3 API中的函数X有属性Y等

The sentence "we proved program X to be correct" is very misleading. The main problem is: what does it mean to be correct. In the case of Z3, one could say that Z3 is correct if, at least, it never returns "sat" for an unsatisfiable problem, and "unsat" for a satisfiable one. This definition may be improved by also including additional properties such as: Z3 should not crash; the function X in the Z3 API has property Y, etc.

在我们就应该证明的内容达成一致后，我们必须创建运行时模型、编程语言语义(在 Z3 的情况下为 C++)等.然后，使用工具(又名验证器)将实际代码转换为一组公式，我们应该使用定理证明器(例如 Z3)来检查这些公式.我们需要验证器，因为 Z3 不理解"C++.验证 C 编译器 (VCC) 是此类工具的一个示例.请注意，使用这种方法证明 Z3 是正确的并不能明确保证 Z3 真的正确，因为我们的模型可能不正确，验证者可能不正确，Z3 可能不正确，等等.

After we agree on what we are supposed to prove, we have to create models of the runtime, programming language semantics (C++ in the case of Z3), etc. Then, a tool (aka verifier) is used to convert the actual code into a set of formulas that we should check using a theorem prover such as Z3. We need the verifier because Z3 does not "understand" C++. The Verifying C Compiler (VCC) is an example of this kind of tool. Note that, proving Z3 to be correct using this approach does not provide a definitive guarantee that Z3 is really correct since our models may be incorrect, the verifier may be incorrect, Z3 may be incorrect, etc.

要使用验证器，例如VCC，我们需要用我们要验证的属性、循环不变量等来注释程序.一些注释用于指定代码片段应该做什么.其他注释用于帮助/指导"定理证明者.在某些情况下，注释的数量大于被验证的程序.因此，该过程不是完全自动的.

To use verifiers, such as VCC, we need to annotate the program with the properties we want to verify, loop invariants, etc. Some annotations are used to specify what code fragments are supposed to do. Other annotations are used to "help/guide" the theorem prover. In some cases, the amount of annotations is bigger than the program being verified. So, the process is not completely automatic.

另一个问题是成本，这个过程会非常昂贵.这将比实施 Z3 更耗时.Z3 有 30 万行代码，其中一些代码基于非常微妙的算法和实现技巧.另一个问题是维护，我们会定期添加新功能并提高性能.这些修改会影响证明.

Another problem is cost, the process would be very expensive. It would be much more time consuming than implementing Z3. Z3 has 300k lines of code, some of this code is based on very subtle algorithms and implementation tricks. Another problem is maintenance, we are regularly adding new features and improving performance. These modifications would affect the proof.

尽管成本可能非常高，但 VCC 已被用于验证重要的代码段，例如 Microsoft Hyper-V 管理程序.

Although the cost may be very high, VCC has been used to verify nontrivial pieces of code such as the Microsoft Hyper-V hypervisor.

理论上，任何编程语言 X 的验证器都可以用来证明自己，如果它也用语言 X 实现.Spec# 验证程序就是此类工具的一个示例.Spec# 是在 Spec# 中实现的，并且 Spec# 的几个部分使用 Spec# 进行了验证.请注意，Spec# 使用 Z3 并假设它是正确的.当然，这是一个很大的假设.

In theory, any verifier for programming language X can be used to prove itself if it is also implemented in language X. The Spec# verifier is an example of such tool. Spec# is implemented in Spec#, and several parts of Spec# were verified using Spec#. Note that, Spec# uses Z3 and assumes it is correct. Of course, this is a big assumption.

您可以在论文中找到有关这些问题和 Z3 应用程序的更多信息:http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf

You can find more information about these issues and Z3 applications on the paper: http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf

这篇关于有没有人试过用 Z3 本身证明 Z3?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！