有人尝试使用Z3证明Z3本身吗？
14
- Longfei Zhu
4
将来请在问题中提供更多信息，以便人们理解你在谈论什么。一方面，我理解你正在询问已经了解Z3的人，但由于那些不知道Z3是什么的人会将这个问题标记为“我甚至不知道是什么...”，所以你必须确保人们知道你在谈论什么，在这种情况下，至少要提供该工具的链接。 - Lasse V. Karlsen
话虽如此，我并不完全确定这个问题是否适合在这里提问，我认为也许[programmers.se]是一个更合适的地方，但我会等待并看看社区的意见。 - Lasse V. Karlsen
@Lasse [cstheory.se] 更像是理论计算机科学。我的哥德尔启发猜想是，任何足够强大而有趣的系统都无法证明自己的正确性。 - AakashM
3正如Leonardo de Moura在他的回答中所概述的那样，“证明Z3”意味着人类提供不变量，然后这些不变量将参与计算验证条件，其有效性将由Z3进行检查。虽然Z3是一种自动证明器，但从某种意义上说，它只是检查不变量的选择，而不是进行证明本身。因此，在这里绝对没有类似于哥德尔的悖论。 - Pascal Cuoq
2个回答
30
简短的回答是：“没有人试图使用Z3证明Z3本身” :-)
句子“我们证明了程序X是正确的”非常误导人。主要问题在于：什么是正确的。对于Z3，可以说如果它至少从不返回“sat”以表示不可满足问题，“unsat”表示可满足问题，则Z3是正确的。此定义可以通过包括其他属性来改进，例如：Z3不应崩溃； Z3 API中的函数X具有属性Y等。
在我们同意我们应该证明什么之后，我们必须创建运行时模型，编程语言语义（在Z3的情况下为C ++）等模型。然后，使用工具（称为验证器）将实际代码转换为一组公式，我们应该使用像Z3这样的定理证明器进行检查。我们需要验证器，因为Z3不“理解”C ++。验证C编译器（VCC）就是这种工具的例子。请注意，使用此方法证明Z3的正确性并不能提供确切的保证，因为我们的模型可能是错误的，验证器可能是错误的，Z3可能是错误的等等。
要使用验证器（如VCC），我们需要用我们想要验证的属性、循环不变量等注释程序。有些注释用于指定代码段应该执行的操作。其他注释用于“帮助/指导”定理证明器。在某些情况下，注释的数量比正在验证的程序还要大。因此，该过程并不完全自动化。
另一个问题是成本，这个过程将非常昂贵。它将比实施Z3更耗时。 Z3有300k行代码，其中一些代码基于非常微妙的算法和实现技巧。 另一个问题是维护，我们定期添加新功能并提高性能。这些修改会影响证明。
尽管成本可能非常高，但VCC已用于验证诸如Microsoft Hyper-V hypervisor之类的复杂代码片段。
理论上，任何编程语言X的验证器都可以用于证明自身，如果它也是用语言X实现的话。 Spec#验证器就是这样一个工具的例子。 Spec#是用Spec#实现的，并且使用了Spec#的几个部分进行了验证。 请注意，Spec#使用Z3并假设它是正确的。当然，这是一个很大的假设。
您可以在这篇论文中找到有关这些问题和Z3应用程序的更多信息： http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf
句子“我们证明了程序X是正确的”非常误导人。主要问题在于：什么是正确的。对于Z3，可以说如果它至少从不返回“sat”以表示不可满足问题，“unsat”表示可满足问题，则Z3是正确的。此定义可以通过包括其他属性来改进，例如：Z3不应崩溃； Z3 API中的函数X具有属性Y等。
在我们同意我们应该证明什么之后，我们必须创建运行时模型，编程语言语义（在Z3的情况下为C ++）等模型。然后，使用工具（称为验证器）将实际代码转换为一组公式，我们应该使用像Z3这样的定理证明器进行检查。我们需要验证器，因为Z3不“理解”C ++。验证C编译器（VCC）就是这种工具的例子。请注意，使用此方法证明Z3的正确性并不能提供确切的保证，因为我们的模型可能是错误的，验证器可能是错误的，Z3可能是错误的等等。
要使用验证器（如VCC），我们需要用我们想要验证的属性、循环不变量等注释程序。有些注释用于指定代码段应该执行的操作。其他注释用于“帮助/指导”定理证明器。在某些情况下，注释的数量比正在验证的程序还要大。因此，该过程并不完全自动化。
另一个问题是成本，这个过程将非常昂贵。它将比实施Z3更耗时。 Z3有300k行代码，其中一些代码基于非常微妙的算法和实现技巧。 另一个问题是维护，我们定期添加新功能并提高性能。这些修改会影响证明。
尽管成本可能非常高，但VCC已用于验证诸如Microsoft Hyper-V hypervisor之类的复杂代码片段。
理论上，任何编程语言X的验证器都可以用于证明自身，如果它也是用语言X实现的话。 Spec#验证器就是这样一个工具的例子。 Spec#是用Spec#实现的，并且使用了Spec#的几个部分进行了验证。 请注意，Spec#使用Z3并假设它是正确的。当然，这是一个很大的假设。
您可以在这篇论文中找到有关这些问题和Z3应用程序的更多信息： http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf
- Leonardo de Moura
3
不，不能使用该工具本身证明非平凡工具的正确性。这基本上在哥德尔第二不完备定理中已经说明：
对于任何形式有效生成的理论T，包括基本算术真理和关于形式可证明性的某些真理，如果T包括自己一致性的陈述，那么T是不一致的。
由于Z3包括算术，因此它无法证明其自身的一致性。
因为它在上面的评论中提到：即使用户提供不变量，哥德尔定理仍然适用。这不是可计算性问题。该定理指出，在一致系统中不存在这样的证明。
但是，您可以使用Z3验证Z3的部分内容。
5年后的编辑：
实际上，这个论点比哥德尔的不完备定理更容易理解。
假设只有当Z3对于不可满足的公式仅返回UNSAT时，Z3才是正确的。
假设我们找到一个公式A，如果A是不可满足的，则Z3是正确的（并且我们已经证明了这种关系）。
我们可以将此公式提供给Z3，但是：
1. 如果Z3返回UNSAT，则可能是因为Z3是正确的或者Z3中存在漏洞。因此我们没有验证任何内容。 2. 如果Z3返回SAT和一个反例模型，则我们可能能够通过分析该模型来发现Z3中的错误。 3. 否则我们什么也不知道。
因此，我们可以使用Z3来查找Z3中的错误，并提高对Z3的信心（达到极高水平），但不能正式验证它。
对于任何形式有效生成的理论T，包括基本算术真理和关于形式可证明性的某些真理，如果T包括自己一致性的陈述，那么T是不一致的。
由于Z3包括算术，因此它无法证明其自身的一致性。
因为它在上面的评论中提到：即使用户提供不变量，哥德尔定理仍然适用。这不是可计算性问题。该定理指出，在一致系统中不存在这样的证明。
但是，您可以使用Z3验证Z3的部分内容。
5年后的编辑：
实际上，这个论点比哥德尔的不完备定理更容易理解。
假设只有当Z3对于不可满足的公式仅返回UNSAT时，Z3才是正确的。
假设我们找到一个公式A，如果A是不可满足的，则Z3是正确的（并且我们已经证明了这种关系）。
我们可以将此公式提供给Z3，但是：
1. 如果Z3返回UNSAT，则可能是因为Z3是正确的或者Z3中存在漏洞。因此我们没有验证任何内容。 2. 如果Z3返回SAT和一个反例模型，则我们可能能够通过分析该模型来发现Z3中的错误。 3. 否则我们什么也不知道。
因此，我们可以使用Z3来查找Z3中的错误，并提高对Z3的信心（达到极高水平），但不能正式验证它。
- Peter Zeller
3
3我们不应将Z3与其实现的逻辑系统混淆：一阶逻辑+理论（如算术）。问题不在于我们能否证明这些逻辑系统的一致性，而在于Z3是否正确。这是两回事。如果对于一个可满足的陈述集合，Z3没有返回“unsat”，我们就可以说Z3是正确的。另外需要注意的是，Z3不支持不变量，不变量被发送到通常实现更强的逻辑系统的软件验证工具中。 - Leonardo de Moura
你如何证明Z3的一致性，而不必展示它的逻辑系统是一致的呢？你可以假设逻辑系统是一致的，但这样只是在假设Z3是正确的前提下证明它是正确的。 - Peter Zeller
是的，我们假设一阶逻辑+算术等理论是一致的。大多数数学家认为这是正确的。当我们谈论Z3的正确性时，我们考虑的是其实现中使用的算法和过程，而不是它所基于的逻辑系统的一致性。最后，正如我在我的答案中指出的那样，正确性的证明必须在另一个“理解”C/C++语义（用于实现Z3的编程语言）的系统中进行。该系统可能使用不同的逻辑系统，甚至可以将Z3作为子程序调用。 - Leonardo de Moura
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接