13

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

甚至有可能使用 Z3 来证明 Z3 是正确的吗？

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

4

2 回答 2

29

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

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

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

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

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

尽管成本可能非常高，但 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

于 2011-08-03T15:47:16.747 回答
2

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

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

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

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

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

5年后编辑：

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

假设 Z3 仅针对无法满足的公式返回 UNSAT 是正确的。

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

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

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

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

于 2013-11-23T13:46:27.567 回答