使用Microsoft代码契约检查不变量

Question

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

Answer 1

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

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

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

系统不会尝试证明可以违反不变量。“未经验证”的错误消息表示没有找到正确的证明。这个不变量可能仍然是真的，只是没有被证明。

因此，没有误报(同样，根据设计，假设没有bug或破坏)。