当十字线命令成功执行时，我的合同是否正确？

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]。