有人尝试过用Z3本身来证明Z3吗？

Question

有人尝试过用Z3本身来证明Z3吗？

有没有可能，使用Z3来证明Z3是正确的？

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

Answer 1

简短的回答是：“不，没有人尝试使用Z3本身来证明Z3”:-)

“我们证明了程序X是正确的”这句话极具误导性。主要的问题是:什么是正确的。在Z3的情况下，可以说Z3是正确的，至少对于不可满足的问题，它永远不会返回“sat”，而对于可满足的问题，它永远不会返回“unsat”。还可以通过包括附加属性来改进此定义，例如: Z3不应崩溃；Z3应用程序接口中的函数X具有属性Y等。

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

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

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

尽管成本可能非常高，但VCC已用于验证Microsoft Hyper-V虚拟机管理程序等重要代码片段。

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

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

Answer 2

不，不可能使用工具本身来证明一个重要的工具是正确的。这基本上是在Gödel's second incompleteness theorem中声明的

对于任何形式有效生成的理论T，包括基本算术真理和关于形式可证明性的某些真理，如果T包括其自身一致性的声明，则T是不一致的。

由于Z3包含算术，因此它无法证明自己的一致性。

因为上面的评论提到了这一点:即使用户提供了不变量，Gödels定理仍然适用。这不是可计算性的问题。该定理指出，在一致的系统中不能存在这样的证明。

但是，您可以使用Z3验证Z3的某些部分。

5年后的编辑：

实际上，这个论点比Gödel的不完全性定理更容易。

假设Z3对于不可满足的公式只返回UNSAT，那么它就是正确的。

假设我们找到一个公式A，如果A是不可满足的，那么Z3是正确的(我们以某种方式证明了这个关系)。

我们可以把这个公式给Z3，但是

1. 如果Z3返回UNSAT，可能是因为Z3是正确的，也可能是因为Z3中的错误。所以我们还没有验证任何东西。
2. 如果Z3返回SAT和一个反模型，我们也许能够通过分析我们什么都不知道的model
3. otherwise来发现Z3中的错误。

因此，我们可以使用Z3来查找Z3中的错误，并提高对Z3的信心(达到极高的水平)，但不能正式验证它。