z3 - 有没有人试过用 Z3 本身证明 Z3？

Question

有没有人试过证明Z3 Z3本身？

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

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

Answer 1

简短的回答是:“不，没有人试图使用 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 有 30 万行代码，其中一些代码基于非常微妙的算法和实现技巧。
另一个问题是维护，我们会定期添加新功能并提高性能。这些修改会影响证明。

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

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

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