当十字准线命令成功时，我的合同是否被证明是正确的？

Question

当crosshair 找不到反例时，它是否使用Z3 求解器来证明我的合同成立？

docs 表示没有反例并不能保证该属性成立，但这仅仅是因为翻译或建模可能不正确吗？

免责声明：我是 CrossHair 的主要贡献者（我只是使用堆栈溢出作为一种公共方式来记录我之前被问到的问题的答案）

Answer 1

除了不健全的建模可能存在许多问题外，CrossHair 不提供此保证。

CrossHair 是一个疯狂的incomplete 系统。在内部，对于每个后置条件，它会生成三个可能的结果：“确认”、“拒绝”和“未知”。它只为“被拒绝”的情况产生输出；因此，没有输出并不表示该语句得到验证。

为什么 CrossHair 会这样工作？两个原因：

1. CrossHair 为除最微不足道的情况之外的所有情况生成“未知”。对于大多数开发人员来说，“未知”和“已确认”之间的区别并不是非常可行。 （至少目前，重构您的代码以使其完全可以被 CrossHair 探索是不可能的或丑陋的）但是请注意，CrossHair 会在产生“未知”结果之前尝试许多执行路径 - 结果仍然提供了一些条件成立的证据。
2. 随着时间的推移，已确认与未知的区别将非常不稳定。 CrossHair 的设计初衷就是为了进化。平均而言，SMT 求解器会变得更好。 CrossHair 会变得更好。但平均而言，两者都会变得更好；对于个别情况，两者都可能变得更糟。为了避免对已确认与未知回归的担忧，默认情况下隐藏了这种区别。

最好将 CrossHair 视为求解器辅助的模糊测试器。

话虽如此，如果您仍想查看哪些属性是可确认的，您可以使用特殊的“全部报告”选项请求此输出：crosshair check --report_all [TARGET]。