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

Question

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

Answer 1

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

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

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

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

所以没有误报（再次，按照设计，假设没有错误或破坏）。