Lon*_*Zhu 11 theorem-proving theorem z3
有没有人尝试用Z3本身证明Z3？
甚至可以使用Z3证明Z3是正确的吗？
更理论化,是否有可能使用X本身来证明工具X是正确的？
Leo*_*ura 27
简短的回答是:"不,没有人试图用Z3本身来证明Z3":-)
句子"我们证明程序X是正确的"是非常误导的.主要问题是:正确是什么意思.在Z3的情况下,如果至少它对于不可满足的问题永远不会返回"sat"而对于可满足的问题则"不满",则可以说Z3是正确的.这个定义可以通过包括其他属性来改进,例如:Z3不应该崩溃; Z3 API中的函数X具有属性Y等.
在我们就我们应该证明什么达成一致之后,我们必须创建运行时模型,编程语言语义(在Z3的情况下为C++)等等.然后,使用工具(aka verifier)将实际代码转换为我们应该使用诸如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