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

Question

有没有人尝试用 Z3 本身证明 Z3 ？

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

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

Answer 1

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

“我们证明了程序 X 是正确的”这句话非常具有误导性。
主要问题是：正确意味着什么？
就 Z3 而言，如果至少对于不可满足的问题它永远不会返回“sat”，对于可满足的问题则返回“unsat”，那么我们可以说 Z3 是正确的。
这个定义可以通过还包括附加属性来改进，例如： Z3 不应崩溃； Z3 API 中的函数 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

不，不可能使用工具本身来证明一个重要的工具是正确的。这基本上在哥德尔第二不完备性定理中得到了阐述：

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

由于Z3包含算术，所以它不能证明其自身的一致性。

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

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

5年后编辑：

其实这个论证比哥德尔不完备定理更容易。

假设 Z3 是正确的，如果它只针对不可满足的公式返回 UNSAT。

假设我们找到一个公式 A，如果 A 不可满足，则 Z3 是正确的（并且我们已经以某种方式证明了这种关系）。

我们可以将此公式提供给 Z3，但

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

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