有没有人尝试证明Z3 http://research.microsoft.com/en-us/um/redmond/projects/z3/与Z3本身？
是否有可能使用 Z3 来证明 Z3 是正确的？
更理论化的是，是否有可能使用 X 本身来证明工具 X 是正确的？
简短的回答是：“不，没有人尝试使用 Z3 本身来证明 Z3”:-)
“我们证明了程序 X 是正确的”这句话非常具有误导性。
主要问题是：正确意味着什么。
就 Z3 而言，如果至少对于不可满足的问题它永远不会返回“sat”，对于可满足的问题则返回“unsat”，那么我们可以说 Z3 是正确的。
这个定义可以通过还包括附加属性来改进，例如： Z3 不应崩溃； Z3 API 中的函数 X 具有属性 Y 等。
在我们就要证明的内容达成一致后，我们必须创建运行时模型、编程语言语义（Z3 中为 C++）等。
然后，使用工具（又名验证器）将实际代码转换为一组公式，我们应该使用定理证明器（例如 Z3）来检查这些公式。
我们需要验证器，因为 Z3 不“理解”C++。
验证 C 编译器 (VCC http://research.microsoft.com/en-us/projects/vcc/）是此类工具的一个示例。
请注意，使用这种方法证明 Z3 是正确的并不能明确保证 Z3 确实正确，因为我们的模型可能不正确，验证器可能不正确，Z3 可能不正确等。
要使用验证器，例如VCC，我们需要用我们想要验证的属性、循环不变量等来注释程序。一些注释用于指定代码片段应该做什么。其他注释用于“帮助/指导”定理证明者。在某些情况下，注释的数量比正在验证的程序还要多。因此，该过程并不是完全自动的。
另一个问题是成本，这个过程会非常昂贵。这比实施 Z3 花费的时间要多得多。
Z3 有 30 万行代码，其中一些代码基于非常微妙的算法和实现技巧。
另一个问题是维护，我们定期添加新功能并提高性能。这些修改会影响证明。
尽管成本可能非常高，但 VCC 已被用于验证重要的代码片段，例如 Microsoft Hyper-V 虚拟机管理程序。
理论上，任何编程语言 X 的验证器如果也是用 X 语言实现的，都可以用来证明自己。
这Spec# http://research.microsoft.com/en-us/projects/specsharp/verifier 就是此类工具的一个例子。
Spec#是在Spec#中实现的，并且Spec#的几个部分是使用Spec#进行验证的。
请注意，Spec# 使用 Z3 并假设它是正确的。当然，这是一个很大的假设。
您可以在论文中找到有关这些问题和 Z3 应用程序的更多信息：http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
