当crosshair命令成功时，我的合同被证明是正确的吗？

Question

当crosshair没有找到反例时，它是否使用了Z3解算器来证明我的合同有效

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

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

Answer 1

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

十字线是一种非常广泛的incomplete系统。在内部，对于每个后置条件，它生成三个可能的结果：“确认”、“拒绝”和“未知”；因此，没有输出并不表示对语句进行了验证

为什么十字线是这样工作的？原因有二：

1. 交叉线为除最琐碎的情况外的所有情况生成“未知”。对于大多数开发人员来说，“未知”和“确认”之间的区别是不可操作的。（至少目前，重构代码以使其完全可由CrossHair进行探索是不可能的或丑陋的）但是，请注意，CrossHair将在生成“未知”结果之前尝试许多执行路径-结果仍然提供了一些证据证明该条件成立
2. 随着时间的推移，确认与未知的区别将非常不稳定。十字线的设计，从一开始，就是为了发展。平均而言，SMT解决方案将变得更好。十字准星会变好的。但平均而言，两者都会变得更好；就个别情况而言，两者都可能恶化。为了避免对确认回归和未知回归的担忧，默认情况下隐藏了这一区别

最好将CrossHair视为一个解算器辅助的模糊测试仪

综上所述，如果您仍然希望看到哪些属性是可确认的，您可以使用一个特殊的“report All”选项请求此输出：crosshair check report_all [TARGET]