刚刚接触到Microsoft Code合约，用于检查代码(https://learn.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts(中的前置条件，后条件和对象不变量，并想尝试一下。我想确认一个关于健全性和完整性的问题，假设检查器不输出任何错误消息是不变量，这是否意味着不变确实(可证明(为真，或者它仍然可能是误报。
静态检查器可以通过各种方式被愚弄，例如添加错误的假设。我将在这个答案中假设没有做过这样的事情。
此外，检查器中可能存在错误。但假设没有...
静态检查器旨在不产生误报。所有前置条件和后置条件以及不变量都将被检查，只有在条件的真实性可以得到肯定验证的情况下，它们才会通过。如果无法验证条件，则将提供错误消息。
系统不会尝试证明可以违反不变量。"未经证实"的错误消息表示未找到正确性证明。不变性可能仍然是正确的，只是未经证实。
所以没有误报(同样，根据设计，假设没有错误或破坏(。