使用 Microsoft 代码合同检查不变量

Question

刚刚了解了用于检查代码中的前置条件、后置条件和对象不变量的 Microsoft 代码合同 ( https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts ) 并想尝试一下。我想确认一个关于稳健性和完整性的问题，假设检查器不输出任何错误消息的不变量，这是否意味着不变量确实（可证明）为真，或者它仍然可能是误报。

Answer 1

可以通过多种方式欺骗静态检查器，例如添加错误假设。我将在这个答案中假设没有做过类似的事情。

此外，检查器中可能存在错误。但假设没有...

静态检查器旨在不产生误报。所有的前置条件和后置条件以及不变量都会被检查，只有当条件的真实性得到肯定验证时它们才会通过。如果无法验证条件，则会提供错误消息。

系统不会试图证明可以违反不变量。“未经证实”的错误消息意味着没有找到正确性的证据。不变量可能仍然是真实的，只是未经证实。

所以没有误报（同样，根据设计，假设没有错误或破坏）。