dafny相应的SMT查询

Question

我试图检查一个在整数数组中找到最大元素的简单循环程序。这是permalink 这里。所有操作都很好，但我对生成的SMT文件非常感兴趣，所以我使用以下方法提取它：

$ dafny /compile:3 /proverLog:./mySMT.smt myCode.dfy

然后使用z3运行，如下所示：

$ z3 ./mySMT.smt

我得到了3个unsat响应，我想知道对应的3个查询是什么？我查看了*.smt文件，发现了11K机器生成的SMT。有破解smt文件的提示吗？谢谢!

Answer 1

如果您想要得到的SMT文件，那么11K文件就是您的答案。我想，查看它会使您得出这样的结论，即您实际上不想查看生成的SMT文件。

所以，我不知道你想做什么。如果您想了解更多关于您的程序，那么最好的方法是工作(仅)从Dafny程序文本。例如，您可以向验证器添加更多的assert语句，在语句的位置是否可以证明给定的条件。

如果您对Dafny如何编码其验证条件感兴趣(也就是说，如果您自己是一个工具开发人员，并且希望学习如何生成良好的验证条件)，那么我建议您使用/print开关来生成Dafny生成的Boogie程序。通过对Boogie中间验证语言的一些理解，Boogie代码是可读的。关于如何将类似Dafny的语言编码为Boogie的更多教程，我建议如下：

“面向对象软件的规范和验证”，K.RustanM.Leino。讲座笔记，Marktoberdorf，2008年。

鲁斯坦

PS。除非坚持特定的格式设置，否则，如果首先将数组的元素转换为序列，则无需使用循环即可打印数组元素：

print "a = ", a[..], "\n";