当crosshair没有找到反例时，它是否使用Z3求解器来证明我的合同成立？
文档表明没有反例并不能保证该属性成立，但这仅仅是因为翻译或建模可能不正确吗？
免责声明：我是 CrossHair 的主要贡献者（我只是使用堆栈溢出作为一种公共方式来记录我以前被问过的问题的答案）
问问题
47 次
1 回答
1
除了可能与不健全的建模有关的许多问题外，CrossHair 不提供此保证。
CrossHair 是一个非常不完整的系统。在内部，对于每个后置条件，它会生成三个可能的结果：“确认”、“拒绝”和“未知”。它只为“被拒绝”的情况产生输出；因此，没有输出并不表明该声明得到了验证。
为什么 CrossHair 会这样工作？两个原因：
- CrossHair 为除最微不足道的情况之外的所有情况生成“未知”。对于大多数开发人员来说，“未知”和“已确认”之间的区别并不是非常可行。（至少目前，重构您的代码以使其完全可以被 CrossHair 探索是不可能的或丑陋的）但是请注意，CrossHair 将在产生“未知”结果之前尝试许多执行路径 - 结果仍然提供了一些条件成立的证据。
- 随着时间的推移，已确认与未知的区别将非常不稳定。CrossHair 的设计初衷就是为了进化。平均而言，SMT 求解器会变得更好。CrossHair 会变得更好。但平均而言，两者都会变得更好；对于个别情况，两者都可能变得更糟。为了避免对已确认与未知回归的担忧，默认情况下隐藏了这种区别。
最好将 CrossHair 视为求解器辅助的模糊测试器。
话虽如此，如果您仍然想查看哪些属性是可确认的，您可以使用特殊的“report all”选项请求此输出：crosshair check --report_all [TARGET].
于 2020-03-01T18:17:44.303 回答